Foundational papers by Henk Barendregt (and co-authors)

Papers and talks on logic and computer science


Towards the range property for the lambda theory H.
In: Calculi, Types and Applications Essays in honour of,
M. Coppo, M. Dezani-Ciancaglini and S. Ronchi Della Rocca.
Edited by Stefano Berardi and Ugo de' Liguoro.
Theoretical Computer Science 398, Elsevier. 2008. pp. 12-15.
Laat de computer wiskundige stellingen bewijzen
Natuurwetenschap & Techniek.
Proofs of correctness in Mathematics and Industry.
To appear in: Wiley Encyclopedia of Computer Science and Engineering. Wiley. 15 pp.
Foundations of Mathematics from the Perspective of Computer Mathematics
To appear in: Festschrift for Bruno Buchberger. Edited by Peter Paule. 15 pp.
Applications of infinitary lambda terms.
To appear in: Festschrift for Giuseppe Longo. Edited by G. Castagna. 31 pp.


Over welke kwestie zijn bijna al uw vakgenoten het oneens met u?


Proofs of Correctness To appear in Wiley Encyclopedia of Computer Science and Engineering.
Bewijzen: Romantisch of Cool (with F. Wiedijk) In: Euclides, 81 (4), 2006, 175-179.


B"ohm's Theorem, Church's Delta, Numeral Systems, and Ershov Morphisms (with R. Statman)
In: Processes, Terms and Cycles: Steps on the Road to Infinity,
Essays Dedicated to Jan Willem Klop on the Occasion of His 60th Birthday,
Eds. A. Middeldorp, V. van Oostrom and F. van Raamsdonk,
Springer LNCS, vol. 3838, 2005, 40-54.
The Challenge of Computer Mathematics (with F. Wiedijk)
In Transactions A of the Royal Society, vol. 363, no. 1835, 2351-2375.



Towards an Interactive Mathematical Proof Language
in: Thirty Five Years of Automath, Ed. F. Kamareddine, Kluwer, 2003, 25-36. (cartoon via advi)


Autarkic computations in formal proofs (with E. Barendsen)
Journal of Automated Reasoning, 28(3), 2002, 321--336. Volume: 35 kb


Electronic Communication of Mathematics and the Interaction of Computer Algebras Systems and Proof Assistants
(with A. Cohen) J. Symbolic Computation, 32 (2001), 3--22.
Proof-checking using Dependent Type Systems (with H. Geuvers)
Handbook of Artificial Reasoning, Volume II, Ch. 18 (2001), 1149--1240. Volume: 490 Kb.
Discriminating coded lambda terms
in: (A. Anderson and M. Zeleny eds.) Logic, Meaning and Computation, Kluwer, 275-285. Volume: 97 kb


Lambda terms for natural deduction, sequent calculus and cut elimination (with S. Ghilezan)
J. Funct. Programming 10 (1) (2000), 121--134. Volume: 80 kb
Communicating mathematics over the web (with A.M. Cohen) (slides of talk)
Proof assistants for mathematics (slides of talk)


Applications of Plotkin terms: partitions and morphisms for closed terms (with R. Statman)
J. Funct. Programming 9 (5) (1999), 565--575.
Problems in type theory
In: Computational Logic, U. Berger and H. Schwichtenberg (eds.), Springer (1999), pp. 99--112. Volume: 85 kb
Lecture: The quest for correctness (slides)
Lecture: Constructing and representing proofs (slides)


Completeness of two systems of illative combinatory logic for first-order propositional and predicate calculus
(with W. Dekkers and M. Bunder) in Archive für Mathematische Logik, 37 (1998), 327--341; Volume: 365 kb
Completeness of the propositions-as-types interpretation of intuitionistic logic into illative combinatory logic
(with W. Dekkers and M. Bunder) in J. Symbolic Logic, 3 (1998), 869--890. (Different contents from previous paper.)
Volume: 373 kb


The impact of the lambda calculus
Bulletin of Symbolic Logic, Volume 3, no 2, 1997, 181--215.
Volume: 164 kb
Computer Wiskunde (in Dutch)
Volume: 50 kb
Tutorial Lambda Calculi with Types (slides)
Volume: 107 kb


The quest for correctness
Images of SMC research, Stichting Mathematisch Centrum,
P.O. Box 94079, 1090 GB Amsterdam, 39--58. Volume: 400 kb.
Kreisel, lambda calculus, a windmill and a castle
Volume: 91 kb
Kreiseliana, about and around Georg Kreisel,
ed. P. Odifreddi, A.K. Peters, Wellesley, Massachusetts, 3--14.


Termination for direct sums of left-linear complete term rewriting systems, Journal of the Association for Computing Machinery 42, No.6, p.1275--1304. (with Y. Toyama and J.W. Klop)
Enumerators of lambda terms are reducing constructively
Annals of Pure and Applied Logic, 73, 3--9. Volume: 84 kb
A two level approach towards lean proof-checking
(with G. Barthe and M. Ruys) Volume: 142 kb.
Types for Proofs and Programs (Types'95),
S. Berardi and M. Coppo (eds.), Springer LNCS 1158, 16--35.


Computable processes
(with H. Mulder and H. Wupper) Volume: 443 kb


Systems of illative combinatory logic complete for first-order propositional and predicate calculus
(with M. Bunder and W. Dekkers) Volume: 141 kb
Journal of Symbolic Logic 58(3) (1993), 89-108.
Constructive proofs of the range property in lambda calculus. A collection of contributions in honour of Corrado Böhm on the occasion of his 70th birthday. Theoret. Comput. Sci. 121, no. 1-2, 59--69.
Theoretical pearls: enumerators of lambda terms are reducing. J. Funct. Programming 2, no. 2, 233--236.


Lambda Calculi with Types
Volume: 362 kb
Representing ``undefined'' in lambda calculus. J. Funct. Programming 2, no. 3, 367--374.


Introduction to generalized type systems. J. Funct. Programming 1, no. 2, 125--154.

Henk Barendregt /