Lambda-Calculus and Combinators: an Introduction(with
Roger Hindley), (Cambridge
Univeristy Press, 2008).
2. New drafts
"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.
3. Recent Papers (Few files are
provided for downloading for papers published in easily available
journals. )
"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.
4. Recent Invited Addresses
"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.
MATHESIS: the Mathematical Foundation for ULYSSES,
RADC-TR-87-223, November, 1987 (interim report, ORA Corporation,
actually published in 1988).
6. Older books
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).
7. Older papers
"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.
Created by J. P. Seldin
Last modified: Wednesday, 26-Mar-2014 14:52:17 MDT
