1.  Recent Books

• Lambda-Calculus and Combinators:  an Introduction (with Roger Hindley), (Cambridge Univeristy Press, 2008).
  

• "Manipulating proofs".  An expository paper on Prawitz normalization and Gentzen cut-elimination for propositional calculus.   Download in gzipped PostScript format or pdf format.
• "How real is the conflict between revealed religion and the theory of evolution", presented at Mistakes of Reason, a conference in honor of John Woods, University of Lethbridge, Alberta, 19-21 April 2002.  Download gzipped PostScript format or pdf format.
• "On normalizing disjunctive intermediate logics", presented at the 39th annual meeting of the Western Canadian Philosophical Association, Calgary, 25-27 October 2002.  Download paper in gzipped PostScript format or pdf format.

• "Type theories from Barendregt's cube for theorem provers", in Luiz Carlos Pereira, Edward Hermann Haeusler, and Valeria de Paiva (editors), Advances in Natural Deduction:  A Celebration of Dag Prawitz's Work, Springer (Trends in Logic, Volume 39), 2014, pp. 129-144.  (See "Recent Invited Addresses" below.)
  
• "Curry's Attitude Towards Popper", Proceedings of the Annual Meeting of the Canadian Society for History and Philosophy of Mathematics, Volume 21, University of British Columbia, Vancouver, BC, 1-3 June 2008,pages 142-149.
• "On the relation between Church-style typing and Curry-style typing.  Submitted to Journal of Applied Logic. Download paper in pdf format or gzipped PostScript format.
  
• "More thoughts on teaching elementary mathematics".  Proceedings of the Annual Meeting of the Canadian Society for History and Philosophy of Mathematics, Volume 20, Concordia University, Montreal, 27-29 July 2007, pages 259-264.  Download paper in pdf format or gzipped PostScript format.
  
• "Thoughts on teaching elementary mathematics".  Proceedings of the Annual Meeting of the Canadian Society for History and Philosophy of Mathematics, Volume 19, York University, Toronto, 28-30 May 2006, pages 242-252.  Download paper in pdf format or gzipped PostScript format.
  
• "The Logic of Church and Curry".  To appear in the Handbook of the History of Logic, volume 5, edited by Dov Gabbay and John Woods, to be published by Elsevier.  Download preprint in gzipped PostScript format or pdf format.
  
• "Curry's Formalism as Structuralism".  Presented to the Thirty-First Annual Meeting of the Canadian Society for History and Philosophy of Mathematics, Waterloo, Ontario, 4-6 June 2005.  Download paper in gzipped PostScript format or pdf format.  Revised version, submitted to Philosophia Mathematica, in gzipped PostScript format or pdf format.
• "Goedel, Kuhn, Popper, and Feyerabend".  Old title, "Goedel, Kuhn, and Feyerabend".  In Ian Jarvie, Karl Milford, and David Miller, editors, Karl Popper:  A Centenary Assessment, vol. II, Ashgate, 2007, pages 87-94.  The paper was presented at Karl Popper 2002, held in Vienna 3-7 July 2002.
• "CURRY, Haskell Brooks (1900-1082)".  Dictionary of Modern American Philosophers, Thoemmes Press, Bristol, England, 2005.  Download paper in gzipped PostScript format or pdf format.
  
• "Informal Incompleteness:  Rules, Philosophy, Law".  Proceedings of the Canadian Society for the History and Philosophy of Mathematics, Volume 17, Thirtieth Annual Meeting, Clare College, Cambridge, 9-11 July, 2004, pages 185-201.  Download paper in gzipped PostScript format or pdf format.
  
• "Interpreting HOL in the calculus of constructions", part of the invited address delivered to conference Thirth-five years of AUTOMATH, Heriot-Watt University, Edinburgh, Scotland, 10-13 April 2002.  Journal of Applied Logic, 2 (2004) 173--189 (Special issue on "Variants of Logics: from HOL to the calculus of constructions to teaching mathematical proofs on computers" edited by F. Kamareddine).  Download paper in gzipped PostScript format or pdf format.
  
• "Variants of the basic calculus of constructions" (with M. W. Bunder).  Journal of Applied Logic, 2 (2004) 191--217 (Special issue on "Variants of Logics: from HOL to the calculus of constructions to teaching mathematical proofs on computers" edited by F. Kamareddine).  Download gzipped PostScript format or pdf format.
• "Curry's anticipation of the types used in programming languages".  Proceedings of the Annual Meeting of the Canadian Society for History and Philosophy of Mathematics, Toronto, 24-26 May 2002, pp. 148-163.  Download slides in gzipped PostScript format or pdf format.  Download paper in gzipped PostScript format (WARNING:  this is a large file) or pdf format.
• "Extensional set equality in the calculus of constructions", Journal of Logic and Computation, 11 (2001) 483--493.  Presented at the Festival Workshop on the Foundations of Computation held at Heriot-Watt University, Edinburgh, July 16-18, 2000.
• "A Gentzen-style sequent calculus of constructions with expansion rules", Theoretical Computer Science243 (2000) 199-215.  Gives a Gentzen-style L-system for the calculus of constructions.
• "On the role of implication in formal logics", Journal of Symbolic Logic65 (2000) 1076-1114.  Shows that the strength of a logical system is largely carried by its rules for implication.
• "On lists and other abstract data types in the calculus of constructions", Mathematical Structures in Computer Science 10 (2000) 261-276 (Special issue in honor of J. Lambek.)  Shows how to interpret the abstract data type lists in the calculus of constructions and extends that interpretation to abstract data types in general.
• "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, pp. 186-191.   Download in gzipped PostScript format or pdf format.
• "Two remarks on ancient Greek geometry", Proceedings of the Annual Meeting of the Canadian Society for History and Philosphy of Mathematics, Brock University, 1996, pp. 26-30.    Download in gzipped PostScript format or pdf format.
• "On the proof theory of Coquand's calculus of constructions", Annals of Pure and Applied Logic 83 (1997) 23-101.

• "Logic and type theory in theorem provers", delivered to conference Thirth-five years of AUTOMATH, Heriot-Watt University, Edinburgh, Scotland, 10-13 April 2002.  See "Interpreting HOL in the Calculus of Constructions" and "Extensionality and the axiom of choice in the calculus of constructions" above.
• "Type theories from Barendregt's cube for theorem provers", delivered at conference Natural Deduction Rio 2001, Rio de Janeiro, 2-6 July 2001.  Slides in gzipped PostScript format or pdf format.  Paper in gzipped PostScript format or pdf format.

• MATHESIS:  the Mathematical Foundation for ULYSSES, RADC-TR-87-223, November, 1987 (interim report, ORA Corporation, actually published in 1988).

• To H. B. Curry:  Essays on Combinatory Logic, Lambda Calculus and Formalism (edited with J. R. Hindley), (Academic Press, London, 1980).
• Introduction to Combinatory Logic (with J. R. Hindley and B. Lercher), London Math. Soc. Lecture Note No. 7, (Cambridge University Press, 1972).  Italian edition:  Introduzione alla Logica Combinatoria, translated by F. Azzarello (Editore Boringhieri,Torino, 1975.
• Combinatory Logic, vol. II (with H. B. Curry and J. R. Hindley), (North-Holland, Amsterdam, 1972).

• "Coquand's calculus of constructions:  a mathematical foundation for a proof development system", Formal Aspects of Computing 4 (1992) 425-441.
• "In memoriam Haskell Brooks Curry", Perspectives on the History of Mathematical Logic, edited by Thomas Drucker (Birkhäuser, Boston, 1991), pp. 169-175.
• "Excluded middle without definite descriptions in the theory of constructions (Extended Abstract)", MWPLT91, Spring, Proceedings of the First Montreal Workshop on Programming Language Theory, April 29-30, 1991, edited by M. Okada and P. J. Scott, pp. 74-83.    Download in gzipped PostScript format or pdf format.
• Article on $\lambda$-calculus and functional programming, Enciclopedia Italiana.  Storia del secolo XX, forthcoming (in Italian).  English draft written in 1991.    Download English draft in gzipped PostScript format or pdf format.
• "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, pp. 120-136.   Download in gzipped PostScript format or pdf format.
• "Reasoning in elementary mathematics", Proceedings of the Annual Meeting of the Canadian Society for History and Philosophy of Mathematics, Université Laval, 1989, pp. 151-174.   Download in gzipped PostScript format or pdf format.
• "Normalization and excluded middle, I", Studia Logica 48 (1989) 193-217.
• "On adding ($\xi$) to weak equality in combinatory logic" (with M. W. Bunder and J. R. Hindley), Journal of Symbolic Logic 54 (1989) 590-607.
• "ULYSSES:  A computer-security modeling environment" (with Tanya Korelsky et al.), Proceedings of the 11th National Computer Security Conference, Baltimore, Maryland, October 17-20, 1988, National Bureau of Standards/National Computer Security Center, 1988, pp. 20-28.
• "Security modelling in the Ulysses environment" (with Tanya Korelsky et al.), Proceedings of the fourth Aerospace Computer Security Applications Conference (Orlando, Florida, December 16-20, 1988), IEEE Computer Society Press, December, 1988, pp. 386-392.
• "A relevant validity in Curry's foundations:  a reply to Richard Sylvan", Bull. Sect. Logic Pol. Acad. Sci. 16 (1987) 68-70.   Download in gzipped PostScript format or pdf format.
• "On the proof theory of the intermediate logic MH", Journal of Symbolic Logic 51 (1986) 626-647.
• "A constructive approach to classical mathematics", Constructive Mathematics edited by F. Richman (Springer Lecture Notes in Math., vol. 873, 1981), pp. 105-110.
• "Curry's program", in To H. B. Curry:  Essays on Combinatory Logic, Lambda Calculus and Formalism edited by J. P. Seldin and J. R. Hindley (Academic Press, London 1980), pp. 3-33.
• "Progress report on generalized functionality", Annals of Mathematical Logic 17 (1979) 29-59.
• "A sequent calculus formulation of type assignment with equality rules for the $\lambda \beta$-calculus", Journal of Symbolic Logic 43 (1978) 643-649.
• "Some anomalies in Fitch's system QD" (with M. W. Bunder), Journal of Symbolic Logic 43 (1978) 247-249.
• "Recent advances in Curry's program", Rend. Sem. Mat. Univers. Politecn. Torino 35 (1976-77) 77-88.
• "A sequent calculus for type assignment", Journal of Symbolic Logic 42 (1977) 11-28.
• "The {\sf Q}-consistency of ${\cal F{_{22}$", Notre Dame Journal of Formal Logic 18 (1977) 117-127.
• "Arithmetic as a study of formal systems", Notre Dame Journal of Formal Logic 16 (1975) 449-464.
• "Equality in ${\cal F}_{22}$", in Logic Colloquium '73 edited by H. E. Rose and J. C. Shepherdson (North-Holland, Amsterdam, 1975), pp. 433-444.
• "Equality in ${\cal F}_{21}$", Journal of Symbolic Logic 38 (1973) 571-575.
• "Note on definitional reductions", Notre Dame Journal of Formal Logic 9 (1968) 4-6.  Corrigenda (to correct typesetting errors) Ibid. 10 (1969) 412 and 21 (1980) 728.