University of Lethbridge

Biography

-- Dr. Math. Nat. Sci. (Equivalent to Ph.D.) University of Amsterdam, 1968.
-- M. A. The Pennsylvania State University, 1966
-- B. A. Oberlin College, Ohio, 1964, Cum Laude.

Jonathan P. Seldin, now Professor Emeritus, is a well-established senior scientist. Combinatory logic, together with lambda-calculus (with which it is equivalent) is a prototype for functional languages, such as LISP and ML, and typed lambda-calculus is a prototype for the typing discipline in programming languages. His work on lambda-calculus, both pure and typed, has applications in formal verification, the use of formal logics to prove properties of programs (e.g., that they satisfy their specifications, which means that they work as they are supposed to). He is also interested in proof normalization and cut-elimination for various systems of formal logic. His work is supported by NSERC.

Selected Publications:
--Seldin, Jonathan P. "Goedel, Kuhn, Popper, and Feyerabend." In Ian Jarvie, Karl Milford, and David Miller (eds), Karl Popper: A Centenary Assessment, volume II, Ashgate, 2007, pages 87-94. (Proceedings of Karl Popper 2002, Vienna, 3--7 July 2002.)
--Seldin, Jonathan P. "Interpreting HOL in the calculus of constructions." Journal of Applied Logic, 2 (2004) 173-189.
--Seldin, Jonathan P. and Bunder, Martin "Variants of the calculus of constructions." Journal of Applied Logic, 2 (2004) 191-217.
--Seldin, Jonathan P. "Extensional set equality in the calculus of constructions." Journal of Logic and Computation. 11 (2001) 483-493.
--Seldin, Jonathan P. "On Lists and Other Abstract Data Types in the Calculus of Constructions." Mathematical Structures in Computer Science. 10 (2000) 261-276.
--Seldin, Jonathan P. "On the Role of Implication in Formal Logics." Journal of Symbolic Logic. 65 (2000) 1076-1114.
--Seldin, Jonathan P. "On the proof theory of Coquand's calculus of constructions." Annals of Pure and Applied Logic 83 (1997) 23-101.
--Hindley, Roger and Jonathan P. Seldin. Introduction to Combinators and lambda-Calculus. Cambridge, England: Cambridge Univeristy Press, 1986.

For a complete list of publications, see my web page (Internet Links below).

Selected Publications

For a complete listing of publications please visit the following website: http://www.cs.uleth.ca/~seldin

Hindley, J. Roger and Seldin, Jonathan P. Lambda-Calculus and Combinators, an Introduction. Cambridge, England, University Press, 2008.

Seldin, Jonathan P. "The Logic of Church and Curry." In Dov Gabbay and John Woods (eds), Handbook of the History of Logic, volume 5, Elsevier, to appear in 2008.

Seldin, Jonathan P. "More thoughts on teaching elementary mathematics." Proceedings of the Canadian Society for History and Philosophy of Mathematics, volume 20, Thirty-second Annual Meeting and Fourth Joint Meeting with the British Society for the History of Mathematics, Concordia University, Montreal, Quebec, July 27--29, 2007, 2008, pages 259-264.

Seldin, Jonathan P. "Thoughts on teaching elementary mathematics." Proceedings of the Canadian Society for History and Philosophy of Mathematics, volume 19, Thirty-first Annual Meeting, York University, Toronto, May 28--30, 2006, 2007, pages 242-252.

Seldin, Jonathan P. "Goedel, Kuhn, Popper, and Feyerabend." In Ian Jarvie, Karl Milford, and David Miller (eds), Karl Popper: A Centenary Assessment, volume II, Ashgate, 2007, pages 87-94. (Proceedings of Karl Popper 2002, Vienna, 3-7 July 2002.)

Seldin, Jonathan P. "Curry's Formalism as Structuralism." Proceedings of the Canadian Society for the History and Philosophy of Mathematics, volume 18, Thirty-First Annual Meeting, Waterloo, Ontario, 4--6 June, 2005,2006, pages 162-172.

Seldin, Jonathan P. "Informal incompleteness: rules, philosophy, and law." Proceedings of the Canadian Society for the History and Philosophy of Mathematics, volume 17, Thirtieth Annual Meeting, Clare College, Cambridge, England, 9--11 July 2004, 2005, pages 185-201.

Seldin, Jonathan P. "Curry, Haskell Brooks (1900-1982)." In Dictionary of Modern American
Philosophers. Thoemmes Press, Bristol, England, 2005.

Seldin, Jonathan P. "Interpreting HOL in the calculus of constructions." Journal of Applied Logic, 2 (2004) 173-189.

Bunder, Martin and Seldin, Jonathan P. "Variants of the calculus of constructions." Journal of Applied Logic, 2 (2004) 191-217.

Seldin, Jonathan P. "Curry's anticipation of types used in programming languages."
Proceedings of the Canadian Society for the History and Philosophy of Mathematics,
Volume 15, Twenty-Eighth Annual Meeting, University of Toronto, Toronto, Ontario, 24--26
May 2002, 2003, pages 148-163.

Seldin, Jonathan P. "Extensional set equality in the calculus of constructions." Journal of Logic and Computation. 11 (2001) 483-493.

Seldin, Jonathan P., "A Gentzen-style sequent calculus of constructions with expansion rules." Theoretical Computer Science. 243 (2000) 199-215.

Seldin, Jonathan P. "On lists and other abstract data types in the calculus of constructions." Mathematical Structures in Computer Science. 10 (2000) 261-276.

Seldin, Jonathan P. "On the Role of Implication in Formal Logics." Journal of Symbolic Logic. 65 (2000) 1076-1114.

Seldin, Jonathan P. "Euclidean geometry before non-Euclidean geometry." Proceedings of the Annual Meeting of the Canadian Society for History and Philosophy of Mathematics, University of Ottawa, 1998,1999, pages 186-191.

Seldin, Jonathan P. "On the proof theory of Coquand's calculus of constructions." Annals of Pure and Applied Logic 83 (1997) 23-101.
Seldin, Jonathan P. "Two remarks on ancient Greek geometry." Proceedings of the Annual Meeting of the Canadian Society for History and Philosophy of Mathematics, Brock University, 1997, 1998, pages 16-30.

Seldin, Jonathan P. "Coquand's calculus of constructions: a mathematical foundation for a proof development system." Formal Aspects of Computing. 4 (1992) 425-441.

Seldin, Jonathan P. "In memoriam Haskell Brooks Curry." In Thomas Drucker (ed.), Perspectives on the History of Mathematical Logic, Birkhaüser, 1991, pages 169-175.

Seldin, Jonathan P. "From exhaustion to modern limit theory." Proceedings of the Annual Meeting of the Canadian Society for History and Philosophy of Mathematics, University of Victoria, BC, 1990, 1991, pages 120-136.

Seldin, Jonathan P. "Reasoning in elementary mathematics." Proceedings of the Annual Meeting of the Canadian Society for History and Philosophy of Mathematics, Université Laval, 1989, 1990, pages 151-174.

Seldin, Jonathan P. "Normalization and excluded middle, I." Studia Logica. 48 (1989) 193-217.

Bunder, M. W. and Hindley, J. Roger and Seldin, Jonathan P. "On adding (ξ) to weak equality in combinatory logic." Journal of Symbolic Logic. 54 (1989) 590-607.

Research Interests

The proof theory of systems of type assignment in lambda-calculus, which has applications in the verification of software and hardware, proof normalization and cut elimination for various systems of formal logic.

Jonathan P. Seldin is a well-established senior scientist. Combinatory logic, together with lambda-calculus (with which it is equivalent) is a prototype for functional languages, such as LISP and ML, and typed lambda-calculus is a prototype for the typing discipline in programming languages. His work on lambda-calculus, both pure and typed, has applications in formal verification, the use of formal logics to prove properties of programs (e.g., that they satisfy their specifications, which means that they work as they are supposed to). He is also interested in proof normalization and cut-elimination for various systems of formal logic. His work is supported by NSERC.

Current Research and Creative Activity

Title	Location	Grant Information	Principal Investigator	Co Researchers
Beta-strong reduction in combinatory logic	Lethbridge, AB
Informal Incompleteness: Rules, Philosophy, Law	Lethbridge, AB	U of L Research Fund, $4500, 2004-2005.	Jonathan P. Seldin, U of L
The history of H.B. Curry's work	Lethbridge, AB
The proof theory of natural deduction systems	Lethbridge, AB
The Relation of Church-style typing and Curry-style typing	Lethbridge, AB

Previous Research

Title	Grant Agency	Completion Date
Cross-Paradigm Investigations in Higher Order Reasoning	Natural Sciences and Engineering Council of Canada	2007

Internet Links

My web page
Department of Mathematics and Computer Science
The University of Lethbridge