Jonathan Seldin
 Faculty
 Mathematics & Computer Science
 Office: B580
(University Hall)
 Phone: (403) 3292364
 Email:
Degrees
Dr. Math. Nat. Sci. (Equivalent to PhD), University of Amsterdam; MA, The Pennsylvania State University; BA Oberlin College, Ohio, Cum LaudeExpertise
Lambdacalculus, combinatory logic, proof theory, history and philosophy of mathematicsResearch Areas
The relation between Churchstyle typing and Currystyle typing, betastrong reduction in combinatory logic, implications of Gödel's incompleteness results for informal reasoning, Curry's attitude towards Popper, normalization of natural deduction proofsPrevious Research Areas
Lambdacalculus, pure and typed, combinatory logic, proof theory, implications of Gödel's incompleteness results for informal reasoning, history and philosophy of the work of H. B. Curry, history and philosophy of mathematicsBiography
 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 wellestablished senior scientist. Combinatory logic, together with lambdacalculus (with which it is equivalent) is a prototype for functional languages, such as LISP and ML, and typed lambdacalculus is a prototype for the typing discipline in programming languages. His work on lambdacalculus, 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 cutelimination 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 8794. (Proceedings of Karl Popper 2002, Vienna, 37 July 2002.)
Seldin, Jonathan P. "Interpreting HOL in the calculus of constructions." Journal of Applied Logic, 2 (2004) 173189.
Seldin, Jonathan P. and Bunder, Martin "Variants of the calculus of constructions." Journal of Applied Logic, 2 (2004) 191217.
Seldin, Jonathan P. "Extensional set equality in the calculus of constructions." Journal of Logic and Computation. 11 (2001) 483493.
Seldin, Jonathan P. "On Lists and Other Abstract Data Types in the Calculus of Constructions." Mathematical Structures in Computer Science. 10 (2000) 261276.
Seldin, Jonathan P. "On the Role of Implication in Formal Logics." Journal of Symbolic Logic. 65 (2000) 10761114.
Seldin, Jonathan P. "On the proof theory of Coquand's calculus of constructions." Annals of Pure and Applied Logic 83 (1997) 23101.
Hindley, Roger and Jonathan P. Seldin. Introduction to Combinators and lambdaCalculus. 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/~seldinHindley, J. Roger and Seldin, Jonathan P. LambdaCalculus 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, Thirtysecond Annual Meeting and Fourth Joint Meeting with the British Society for the History of Mathematics, Concordia University, Montreal, Quebec, July 2729, 2007, 2008, pages 259264.
Seldin, Jonathan P. "Thoughts on teaching elementary mathematics." Proceedings of the Canadian Society for History and Philosophy of Mathematics, volume 19, Thirtyfirst Annual Meeting, York University, Toronto, May 2830, 2006, 2007, pages 242252.
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 8794. (Proceedings of Karl Popper 2002, Vienna, 37 July 2002.)
Seldin, Jonathan P. "Curry's Formalism as Structuralism." Proceedings of the Canadian Society for the History and Philosophy of Mathematics, volume 18, ThirtyFirst Annual Meeting, Waterloo, Ontario, 46 June, 2005,2006, pages 162172.
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, 911 July 2004, 2005, pages 185201.
Seldin, Jonathan P. "Curry, Haskell Brooks (19001982)." 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) 173189.
Bunder, Martin and Seldin, Jonathan P. "Variants of the calculus of constructions." Journal of Applied Logic, 2 (2004) 191217.
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, TwentyEighth Annual Meeting, University of Toronto, Toronto, Ontario, 2426
May 2002, 2003, pages 148163.
Seldin, Jonathan P. "Extensional set equality in the calculus of constructions." Journal of Logic and Computation. 11 (2001) 483493.
Seldin, Jonathan P., "A Gentzenstyle sequent calculus of constructions with expansion rules." Theoretical Computer Science. 243 (2000) 199215.
Seldin, Jonathan P. "On lists and other abstract data types in the calculus of constructions." Mathematical Structures in Computer Science. 10 (2000) 261276.
Seldin, Jonathan P. "On the Role of Implication in Formal Logics." Journal of Symbolic Logic. 65 (2000) 10761114.
Seldin, Jonathan P. "Euclidean geometry before nonEuclidean geometry." Proceedings of the Annual Meeting of the Canadian Society for History and Philosophy of Mathematics, University of Ottawa, 1998,1999, pages 186191.
Seldin, Jonathan P. "On the proof theory of Coquand's calculus of constructions." Annals of Pure and Applied Logic 83 (1997) 23101.
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 1630.
Seldin, Jonathan P. "Coquand's calculus of constructions: a mathematical foundation for a proof development system." Formal Aspects of Computing. 4 (1992) 425441.
Seldin, Jonathan P. "In memoriam Haskell Brooks Curry." In Thomas Drucker (ed.), Perspectives on the History of Mathematical Logic, Birkhaüser, 1991, pages 169175.
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 120136.
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 151174.
Seldin, Jonathan P. "Normalization and excluded middle, I." Studia Logica. 48 (1989) 193217.
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) 590607.
Research Interests
The proof theory of systems of type assignment in lambdacalculus, 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 wellestablished senior scientist. Combinatory logic, together with lambdacalculus (with which it is equivalent) is a prototype for functional languages, such as LISP and ML, and typed lambdacalculus is a prototype for the typing discipline in programming languages. His work on lambdacalculus, 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 cutelimination 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 

Betastrong reduction in combinatory logic  Lethbridge, AB  
Informal Incompleteness: Rules, Philosophy, Law  Lethbridge, AB 
U of L Research Fund, $4500, 20042005.

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 Churchstyle typing and Currystyle typing  Lethbridge, AB 
Previous Research
Title  Grant Agency  Completion Date 

CrossParadigm Investigations in Higher Order Reasoning  Natural Sciences and Engineering Council of Canada  2007 