In the 5th Program Visualization Workshop, Madrid, 2008. Also published in Electronic Notes in Computer Science, Volume 224, #1 January 2009, Pages 115-124. A revised version was published in TOCE.

PDF

HARPO/L: A Language for Hardware/Software Co-design
T. S. Norvell, Xiangwen Li, Dianyong Zhang, Md. Ashraful Alam Tuhin
November 2008

Newfoundland and Labrador Electrical and Computer Engineering Conference, 2008.

PDF

Compiling Parallel Applications to Coarse-Grained Reconfigurable Architectures
Mohammed Ashraful Alam Tuhin and Theodore S. Norvell
May 2008

Canadian Electrical and Computer Engineering Conference, 2008.

PDF

Better monitors for Java
Theodore S. Norvell
October 2007

JavaWorld, October 2007 .

HTML

Formal Derivation of Dynamic Programming Algorithms
Leila Mofarah-Fathi and Theodore S. Norvell
November 2007

Newfoundland and Labrador Electrical and Computer Engineering Conference, 2007.

PDF

Developing Mental Models of Computer Programming Interactively Via the Web
Michael P. Bruce-Lockhart and Theodore S. Norvell
September 2007

IEEE Frontiers in Education , 2007.

PDF

An Intermediate Representation for CGRA implementation
Dianyong Zhang and Theodore S. Norvell
November 2004

Newfoundland and Labrador Electrical and Computer Engineering Conference, 2006.

PDF not yet available

Mapping Applications to Coarse-Grain Reconfigurable Architectures
Mohammed Ashraful Alam Tuhin and Theodore S. Norvell
November 2006

Newfoundland and Labrador Electrical and Computer Engineering Conference, 2006.

PDF

Program and Algorithm Visualization in Engineering and Physics
Michael P. Bruce-Lockhart, Theodore S. Norvell, and Yiannis Cotronis
July 2006

Fourth Program Visualization Workshop 2006, Florence Italy. Also published in Electronic Notes in Theoretical Computer Science. vol. 179. pp. 111--119, 2007.

PDF

Faster searching by elimination
Theodore S. Norvell
October 2005

Newfoundland Electrical and Computer Engineering Conference, 2005.

PDF

So, you want to test your compiler?
Theodore S. Norvell
October 2005

Newfoundland Electrical and Computer Engineering Conference, 2005.

PDF

A Differential Attack on the CIKS-1 Block Cipher
Brian J. Kidney, Howard M. Heys, and Theodore S. Norvell
April 2004

Canadian Electrical and Computer Engineering Conference, 2004.

PDF

Teaching Computer Programming with Program Animation
March 2004
Theodore S. Norvell and Michael P. Bruce-Lockhart

Canadian Conference on Computer and Software Engineering, Calgary, 2004.;

PDF

Open XML Requirements Specifications, a Xylia Based Application
Naeim Semsarilar, Theodore S. Norvell, and Dennis Peters
November 2003

Newfoundland Electrical and Computer Engineering Conference, 2003.

PDF

A Weight Based Attack on the CIKS-1 Block Cipher
Brian J. Kidney, Howard M. Heys, and Theodore S. Norvell
November 2003

Newfoundland Electrical and Computer Engineering Conference, 2003.

PDF

Genericity in Imperative Programs and Logics of Imperative Programs
Theodore S. Norvell
November 2003

Newfoundland Electrical and Computer Engineering Conference, 2003.

[Not available here]

Automating Regression Testing of Java Programs the JSnoopy Way
Theodore S. Norvell
November 2003

Newfoundland Electrical and Computer Engineering Conference, 2003.

PDF

Edits in Xylia: Preserving the Validity of XML Documents
Pouria Shaker, Theodore S. Norvell, and Dennis Peters
November 2002

Newfoundland Electrical and Computer Engineering Conference, 2002.

PDF

The Xylia Toolkit, combining XML and Java
Jonathan Milley, Theodore S. Norvell, and Dennis Peters
November 2001

Newfoundland Electrical and Computer Engineering Conference, 2001.

PDF

program2circuit
July 2001
Eric C. R. Hehner and Theodore S. Norvell

Fifth WSES/IEEE World Multiconference on Circuits, Systems, Communications, and Computers, Crete, 2001 July 8-14, and chapter in Advances in Systems Science: Measurement, Circuits and Control WSES Press Electrical and Computer Engineering Series, p.346-353, 2001

PDF

High-Level Circuit Design
Eric C. R. Hehner, Theodore S. Norvell, and Richard F. Paige
In Programming Methodology, edited by Carroll Morgan and Annabelle McIver, Springer-Verlag, 2002

Abstract: Two compilation schemes from parallel imperative languages to asynchronous circuits.

PDF

A General Framework for Group Robotics with Applications in Mining
J. King, R. Hale, J. Seshadri, R. Gosine, T. Norvell, S. OYoung, A. Fisher,
2000

SPIE Conference on Mobile Robots and Autonomous Systems, 2000.

[Not available.]

Discrete Event Control of Mobile Robotic Systems with Potential Applications in Healthcare
F. Hwang, J. King, R. Hale, M. Rokonuzzaman, R. Gosine, T. Norvell, S. OYoung, and A. Fisher
2000

Digest of Papers of the 2000 World Congress on Medical Physics and Biomedical Engineering and the Proceedings of the 22nd Annual International Conference of the IEEE Engineering in Medicine and Biology Society, July 23-28, 2000, Chicago, Illinois, USA.

[Not available.]

Lifting the hood of the computer: Program animation with the Teaching Machine
Theodore S. Norvell and Michael P. Bruce-Lockhart
May 2000

Canadian Conference on Electrical and Computer Engineering, 2000..

PDF

On the Implementability of Behavioural Systems Preliminary Report
Siu O'Young and Theodore S. Norvell
October 1999

Newfoundland Electrical and Computer Engineering Conference, 1999.

Overheads from the talk (PDF)

An Environment for Proving and Programming
Theodore S. Norvell and Zhikai (Jack) Ding
October 1999

Newfoundland Electrical and Computer Engineering Conference, 1999.

Postscript - PDF

Translating SMALL Programs into FPGA Configurations
Ying Shen and Theodore S. Norvell
October 1999

Newfoundland Electrical and Computer Engineering Conference, 1999.

Postscript - PDF - Talk Overheads (PDF)

Proof by Programming
Theodore S. Norvell
January 1999

Abstract: If you have any conjecture to prove, there is a programming problem such that, if a program can be written that demonstrably solves the programming problem, then the conjecture is true.

This observation leads to a new way of writing proofs and allows tools and techniques developed for the writing of demonstrably correct programs to be applied to proving theorems that ostensibly have nothing to do with programming.

In particular techniques of problem decomposition used in structured programming can be applied to structuring proofs.

This approach neither enlarges nor shrinks the set of theorems provable in a given logic.

What it does is provide a nice way to communicate the structure and content of a proof.

MUNCENTRE Tech Report, January 1999.

Postscript - PDF - DVI

SMALL: A Programming Language for State Machine Design
Theodore S. Norvell
May 1997

Abstract: A new ``hardware-oriented'' programming language is presented. This language allows expression of hardware designs at a register-transfer level with sequencing constructs such as are found in high-level programming languages --including parallelism. The semantics can be defined by any of three different mappings: to predicates, to schematics, and to ASM charts.

Proceedings of the 1997 Canadian Conference on Electrical and Computer Engineering (CCECE/CCGEI) in St. John's, Newfoundland.

PDF - Compressed Postscript - Postscript - Compressed DVI - DVI

The Predicative Semantics of Loops
Theodore S. Norvell
February 1997

Abstract: Introduces and proves a programming law for while-loops that is not based on invariants. The law depends on a semantics of while loops which I call the weakest progressive fixpoint. I also prove that implementability (feasibility) is preserved by while loops under this semantics.

Presented at the 1997 Conference on Algorithmic Languages and Calculi in Le Bischenberg, Alsace.

In: Algorithmic Languages and Calculi, Richard Bird and Lambert Meertens Eds., Chapman-Hall, 1997.

PDF - Postscript - Compressed DVI - DVI

On Trace Specifications
Theodore S. Norvell
July 1995

Abstract: This report explores some ideas for formally specifying modules based on the Trace Assertion Method of Parnas and others.

Published as technical report 305 of the Communications Research Laboratory, McMaster University, July 1995.

PDF - Compressed Postscript - Postscript

Machine Code Programs are Predicates Too
Theodore S. Norvell
January 1994

Abstract: I present an interpretation of machine language programs as boolean expression. Source language programs may also be so interpreted. The correctness of a code generator can then be expressed as a simple relationship between boolean expressions. Code generators can then be calculated from their specifications.

Published in Proceeding of the 6th Refinement Workshop, January 1994, David Till (Ed.), Workshops in Computing, Springer-Verlag, 1994.

PDF - Compressed Postscript - Postscript - Compressed DVI - DVI

A Predicative Theory of Machine Language and its Application to Compiler Correctness
Theodore S. Norvell
1994

Abstract: Presents a method for describing the meaning of machine code programs by interpreting them as predicates. This is used to develop a code generator for a compiler.

University of Toronto PhD Thesis 1994

Not yet available electronically.

Induce-Statements and Induce-Expressions: Constructs for Inductive Programming
Theodore S. Norvell
December 1993

Abstract: Control constructs based on mathematical induction are presented for both imperative and functional languages. These constructs are highly expressive, yet must terminate. They are also quite natural to use for in many situations.

Published in Foundations of Software Technology and Theoretical Computer Science, 13th conference, Bombay, India, December 1993, R.K. Shyamasundar (Ed.), Lecture Notes in Computer Science 761, Springer-Verlag, 1993.

PDF - Compressed Postscript - Postscript - Compressed DVI - DVI
All examples from the paper, rewritten in Gofer

Logical Specifications for Functional Programs
Theodore S. Norvell and Eric C. R. Hehner
June 1992

Abstract: It is shown how to write behavioural specifications for functional programs using first order logic and how to develop executable programs from such specifications.

Published in Mathematics of Program Construction, second international conference, Oxford, U.K., June/July 1992, R.S. Bird, C.C. Morgan, J.C.P. Woodcock (Eds.), Lecture Notes in Computer Science 669, Springer-Verlag, 1993.

PDF - Compressed Postscript - Postscript - Compressed DVI - DVI

Aggregative Closure: An Extension of Transitive Closure
Isabel F. Cruz and Theodore S. Norvell
1989

Abstract: We explore aggregative closure: an abstract problem class that encompasses transitive closure, shortest-path, critical path and other useful problem. We present various abstract algorithms.

Published in Data Engineering, Fifth international conference, Los Angeles, IEEE, 1989.

Not available electronically at the moment.

ProTem
Eric C. R. Hehner and Theodore S. Norvell
1988

Abstract: Discusses the design and semantics of the ProTem programming language.

Published as TR-213 by the Computer Systems Research Institute in Toronto.

Not available electronically.

Expressions, Types, and Data Structures in ProTem
Theodore S. Norvell
1988

Abstract: I discuss the design and semantics of the expression sublanguage of ProTem. Contributions include a unified treatment of recursion in types, data, and functional programs.

Masters Thesis University of Toronto.

Not available electronically.

	THEODORE S. NORVELL
	PUBLICATIONS

Home Contact Research Publications Courses Students Software Informal Publications Miscellanea	Publications See also my Google Scholar profile. Making GUIs less messy: a preliminary report on the Take Back Control library Theodore. S. Norvell Newfoundland and Labrador Electrical and Computer Engineering Conference, 2015. PDF The website for this project. Pipelining inter-iteration dependence in loops onto CGRAs using recurrence-aware priority scheme Rani Gnanaolivu , Theodore. S. Norvell, and Ramachandran Venkatesan Newfoundland and Labrador Electrical and Computer Engineering Conference, 2011. Analysis of Inner-Loop Mapping onto Course-Grained Reconfigurable Architectures using Hybrid Particle Swarm Optimization Rani Gnanaolivu , Theodore. S. Norvell, and Ramachandran Venkatesan International Journal of Organizational and Collective Intelligence. Volume 2, Issue 2, 2011. PDF Modulo Scheduling for Loops with Conditional Branches onto Coarse-Grained Reconfigurable Architectures Rani Gnanaolivu , Theodore. S. Norvell, and Ramachandran Venkatesan Newfoundland and Labrador Electrical and Computer Engineering Conference, 2010. Information Visualization with JHigraph — a progress report Theodore. S. Norvell andM. P. Bruce-Lockhart Newfoundland and Labrador Electrical and Computer Engineering Conference, 2010. PDF revised Dec 2010. Mapping loops onto coarse-grained reconfigurable architectures using particle swarm optimization Rani Gnanaolivu , Theodore. S. Norvell, and Ramachandran Venkatesan Soft computing and pattern recognition. 2010. PDF Adding Test Generation to the Teaching Machine M. P. Bruce-Lockhart, P. Crescenzi, and T. S. Norvell June 2009 ACM Transactions on Computing Education. Volume 9 , Issue 2, June 2009. PDF A grainless semantics for the HARPO/L language Theodore S. Norvell May 2009 Canadian Electrical and Computer Engineering Conference, 2009. PDF Rich Content Plug-ins for the Teaching Machine M. P. Bruce-Lockhart, P. Crescenzi, and T. S. Norvell July 2009 Innovation and Technology in Computer Science Education. PDF Integrating test generation functionality into the Teaching Machine environment M. P. Bruce-Lockhart, P. Crescenzi, and T. S. Norvell July 2008 In the 5th Program Visualization Workshop, Madrid, 2008. Also published in Electronic Notes in Computer Science, Volume 224, #1 January 2009, Pages 115-124. A revised version was published in TOCE. PDF HARPO/L: A Language for Hardware/Software Co-design T. S. Norvell, Xiangwen Li, Dianyong Zhang, Md. Ashraful Alam Tuhin November 2008 Newfoundland and Labrador Electrical and Computer Engineering Conference, 2008. PDF Compiling Parallel Applications to Coarse-Grained Reconfigurable Architectures Mohammed Ashraful Alam Tuhin and Theodore S. Norvell May 2008 Canadian Electrical and Computer Engineering Conference, 2008. PDF Better monitors for Java Theodore S. Norvell October 2007 JavaWorld, October 2007 . HTML Formal Derivation of Dynamic Programming Algorithms Leila Mofarah-Fathi and Theodore S. Norvell November 2007 Newfoundland and Labrador Electrical and Computer Engineering Conference, 2007. PDF Developing Mental Models of Computer Programming Interactively Via the Web Michael P. Bruce-Lockhart and Theodore S. Norvell September 2007 IEEE Frontiers in Education , 2007. PDF An Intermediate Representation for CGRA implementation Dianyong Zhang and Theodore S. Norvell November 2004 Newfoundland and Labrador Electrical and Computer Engineering Conference, 2006. PDF not yet available Mapping Applications to Coarse-Grain Reconfigurable Architectures Mohammed Ashraful Alam Tuhin and Theodore S. Norvell November 2006 Newfoundland and Labrador Electrical and Computer Engineering Conference, 2006. PDF Program and Algorithm Visualization in Engineering and Physics Michael P. Bruce-Lockhart, Theodore S. Norvell, and Yiannis Cotronis July 2006 Fourth Program Visualization Workshop 2006, Florence Italy. Also published in Electronic Notes in Theoretical Computer Science. vol. 179. pp. 111--119, 2007. PDF Faster searching by elimination Theodore S. Norvell October 2005 Newfoundland Electrical and Computer Engineering Conference, 2005. PDF So, you want to test your compiler? Theodore S. Norvell October 2005 Newfoundland Electrical and Computer Engineering Conference, 2005. PDF A Differential Attack on the CIKS-1 Block Cipher Brian J. Kidney, Howard M. Heys, and Theodore S. Norvell April 2004 Canadian Electrical and Computer Engineering Conference, 2004. PDF Teaching Computer Programming with Program Animation March 2004 Theodore S. Norvell and Michael P. Bruce-Lockhart Canadian Conference on Computer and Software Engineering, Calgary, 2004.; PDF Open XML Requirements Specifications, a Xylia Based Application Naeim Semsarilar, Theodore S. Norvell, and Dennis Peters November 2003 Newfoundland Electrical and Computer Engineering Conference, 2003. PDF A Weight Based Attack on the CIKS-1 Block Cipher Brian J. Kidney, Howard M. Heys, and Theodore S. Norvell November 2003 Newfoundland Electrical and Computer Engineering Conference, 2003. PDF Genericity in Imperative Programs and Logics of Imperative Programs Theodore S. Norvell November 2003 Newfoundland Electrical and Computer Engineering Conference, 2003. [Not available here] Automating Regression Testing of Java Programs the JSnoopy Way Theodore S. Norvell November 2003 Newfoundland Electrical and Computer Engineering Conference, 2003. PDF Edits in Xylia: Preserving the Validity of XML Documents Pouria Shaker, Theodore S. Norvell, and Dennis Peters November 2002 Newfoundland Electrical and Computer Engineering Conference, 2002. PDF The Xylia Toolkit, combining XML and Java Jonathan Milley, Theodore S. Norvell, and Dennis Peters November 2001 Newfoundland Electrical and Computer Engineering Conference, 2001. PDF program2circuit July 2001 Eric C. R. Hehner and Theodore S. Norvell Fifth WSES/IEEE World Multiconference on Circuits, Systems, Communications, and Computers, Crete, 2001 July 8-14, and chapter in Advances in Systems Science: Measurement, Circuits and Control WSES Press Electrical and Computer Engineering Series, p.346-353, 2001 PDF High-Level Circuit Design Eric C. R. Hehner, Theodore S. Norvell, and Richard F. Paige In Programming Methodology, edited by Carroll Morgan and Annabelle McIver, Springer-Verlag, 2002 Abstract: Two compilation schemes from parallel imperative languages to asynchronous circuits. PDF A General Framework for Group Robotics with Applications in Mining J. King, R. Hale, J. Seshadri, R. Gosine, T. Norvell, S. OYoung, A. Fisher, 2000 SPIE Conference on Mobile Robots and Autonomous Systems, 2000. [Not available.] Discrete Event Control of Mobile Robotic Systems with Potential Applications in Healthcare F. Hwang, J. King, R. Hale, M. Rokonuzzaman, R. Gosine, T. Norvell, S. OYoung, and A. Fisher 2000 Digest of Papers of the 2000 World Congress on Medical Physics and Biomedical Engineering and the Proceedings of the 22nd Annual International Conference of the IEEE Engineering in Medicine and Biology Society, July 23-28, 2000, Chicago, Illinois, USA. [Not available.] Lifting the hood of the computer: Program animation with the Teaching Machine Theodore S. Norvell and Michael P. Bruce-Lockhart May 2000 Canadian Conference on Electrical and Computer Engineering, 2000.. PDF On the Implementability of Behavioural Systems Preliminary Report Siu O'Young and Theodore S. Norvell October 1999 Newfoundland Electrical and Computer Engineering Conference, 1999. Overheads from the talk (PDF) An Environment for Proving and Programming Theodore S. Norvell and Zhikai (Jack) Ding October 1999 Newfoundland Electrical and Computer Engineering Conference, 1999. Postscript - PDF Translating SMALL Programs into FPGA Configurations Ying Shen and Theodore S. Norvell October 1999 Newfoundland Electrical and Computer Engineering Conference, 1999. Postscript - PDF - Talk Overheads (PDF) Proof by Programming Theodore S. Norvell January 1999 Abstract: If you have any conjecture to prove, there is a programming problem such that, if a program can be written that demonstrably solves the programming problem, then the conjecture is true. This observation leads to a new way of writing proofs and allows tools and techniques developed for the writing of demonstrably correct programs to be applied to proving theorems that ostensibly have nothing to do with programming. In particular techniques of problem decomposition used in structured programming can be applied to structuring proofs. This approach neither enlarges nor shrinks the set of theorems provable in a given logic. What it does is provide a nice way to communicate the structure and content of a proof. MUNCENTRE Tech Report, January 1999. Postscript - PDF - DVI SMALL: A Programming Language for State Machine Design Theodore S. Norvell May 1997 Abstract: A new ``hardware-oriented'' programming language is presented. This language allows expression of hardware designs at a register-transfer level with sequencing constructs such as are found in high-level programming languages --including parallelism. The semantics can be defined by any of three different mappings: to predicates, to schematics, and to ASM charts. Proceedings of the 1997 Canadian Conference on Electrical and Computer Engineering (CCECE/CCGEI) in St. John's, Newfoundland. PDF - Compressed Postscript - Postscript - Compressed DVI - DVI The Predicative Semantics of Loops Theodore S. Norvell February 1997 Abstract: Introduces and proves a programming law for while-loops that is not based on invariants. The law depends on a semantics of while loops which I call the weakest progressive fixpoint. I also prove that implementability (feasibility) is preserved by while loops under this semantics. Presented at the 1997 Conference on Algorithmic Languages and Calculi in Le Bischenberg, Alsace. In: Algorithmic Languages and Calculi, Richard Bird and Lambert Meertens Eds., Chapman-Hall, 1997. PDF - Postscript - Compressed DVI - DVI On Trace Specifications Theodore S. Norvell July 1995 Abstract: This report explores some ideas for formally specifying modules based on the Trace Assertion Method of Parnas and others. Published as technical report 305 of the Communications Research Laboratory, McMaster University, July 1995. PDF - Compressed Postscript - Postscript Machine Code Programs are Predicates Too Theodore S. Norvell January 1994 Abstract: I present an interpretation of machine language programs as boolean expression. Source language programs may also be so interpreted. The correctness of a code generator can then be expressed as a simple relationship between boolean expressions. Code generators can then be calculated from their specifications. Published in Proceeding of the 6th Refinement Workshop, January 1994, David Till (Ed.), Workshops in Computing, Springer-Verlag, 1994. PDF - Compressed Postscript - Postscript - Compressed DVI - DVI A Predicative Theory of Machine Language and its Application to Compiler Correctness Theodore S. Norvell 1994 Abstract: Presents a method for describing the meaning of machine code programs by interpreting them as predicates. This is used to develop a code generator for a compiler. University of Toronto PhD Thesis 1994 Not yet available electronically. Induce-Statements and Induce-Expressions: Constructs for Inductive Programming Theodore S. Norvell December 1993 Abstract: Control constructs based on mathematical induction are presented for both imperative and functional languages. These constructs are highly expressive, yet must terminate. They are also quite natural to use for in many situations. Published in Foundations of Software Technology and Theoretical Computer Science, 13th conference, Bombay, India, December 1993, R.K. Shyamasundar (Ed.), Lecture Notes in Computer Science 761, Springer-Verlag, 1993. PDF - Compressed Postscript - Postscript - Compressed DVI - DVI All examples from the paper, rewritten in Gofer Logical Specifications for Functional Programs Theodore S. Norvell and Eric C. R. Hehner June 1992 Abstract: It is shown how to write behavioural specifications for functional programs using first order logic and how to develop executable programs from such specifications. Published in Mathematics of Program Construction, second international conference, Oxford, U.K., June/July 1992, R.S. Bird, C.C. Morgan, J.C.P. Woodcock (Eds.), Lecture Notes in Computer Science 669, Springer-Verlag, 1993. PDF - Compressed Postscript - Postscript - Compressed DVI - DVI Aggregative Closure: An Extension of Transitive Closure Isabel F. Cruz and Theodore S. Norvell 1989 Abstract: We explore aggregative closure: an abstract problem class that encompasses transitive closure, shortest-path, critical path and other useful problem. We present various abstract algorithms. Published in Data Engineering, Fifth international conference, Los Angeles, IEEE, 1989. Not available electronically at the moment. ProTem Eric C. R. Hehner and Theodore S. Norvell 1988 Abstract: Discusses the design and semantics of the ProTem programming language. Published as TR-213 by the Computer Systems Research Institute in Toronto. Not available electronically. Expressions, Types, and Data Structures in ProTem Theodore S. Norvell 1988 Abstract: I discuss the design and semantics of the expression sublanguage of ProTem. Contributions include a unified treatment of recursion in types, data, and functional programs. Masters Thesis University of Toronto. Not available electronically.	MASc Computer Engineering The Teaching Machine Memorial U. Fencing Club Allez! Fencing Club Source Phile The JavaCC FAQ Turtle World Research Gate Google Scholar Send me money