Foundational papers by Henk Barendregt (and co-authors)
Papers and talks on logic and computer science
-
[2008]
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.
[2007]
Over welke kwestie zijn bijna al uw vakgenoten het oneens met u?
-
[2006]
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. -
[2005]
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.
-
[2004]
-
[2003]
Towards
an Interactive Mathematical Proof Language
in: Thirty Five
Years of Automath, Ed. F. Kamareddine, Kluwer, 2003, 25-36.
(cartoon via advi)[2002]
Autarkic computations in formal proofs
(with E. Barendsen)
Journal of Automated Reasoning, 28(3), 2002, 321--336. Volume: 35 kb
[2001]
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
[2000]
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)
[1999]
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)
[1998]
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
[1997]
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
[1996]
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.
[1995]
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.
[1994]
Computable processes
(with H. Mulder and H. Wupper) Volume: 443 kb
[1993]
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.
[1992]
Lambda Calculi with Types
Handbook of logic in computer science, volume 2. Eds. Abramsky,
Gabbai, Maibaum. Oxford University Press.
Representing ``undefined'' in lambda calculus.
J. Funct. Programming 2, no. 3, 367--374.
[1991]
Introduction to generalized type systems.
J. Functional Programming 1, no. 2, 125--154.
Henk Barendregt /
henk@cs.ru.nl