| |
Publications
Selected Publications by R.P. Nederpelt.
Contact the author on how to receive paper or pdf/postscript versions
of the Articles and Reports
Books:
| 2014 |
Rob Nederpelt and Herman Geuvers:
Type Theory and Formal Proof. An Introduction.
Cambridge University Press, Cambridge, 2014.
ISBN 978-1-107-03650-5, xxviii + 436 pages |
| 2011 |
Rob Nederpelt and Fairouz Kamareddine:
Logical Reasoning: A First Course, Second revised edition.
Texts in Computing, Vol. 3
College Publications, London, 2011.
ISBN 0-954-3006-7-X, xvii + 386 pages |
| 2004 |
Fairouz Kamareddine, Twan Laan, Rob Nederpelt:
A Modern Perspective on Type Theory
From its Origins until Today
Applied Logic Series, Vol. 29
Kluwer Academic Publishers, Dordrecht, 2004.
ISBN 1-4020-2334-0, xiv + 357 pages |
| 1994 |
R.P. Nederpelt, J.H. Geuvers, R.C. de Vrijer (eds.):
Selected
Papers on Automath.
North-Holland, Amsterdam, 1994.
ISBN 0-444-898220, xix + 1024 pages |
Articles:
| 2022 |
Herman Geuvers, Rob Nederpelt
Characteristics of de Bruijn's early proof checker Automath
Fundamenta Informaticae, Vol. 185 (4), pp. 313-336.
2022 |
| 2013 |
Herman Geuvers, Rob Nederpelt
N.G. de Bruijn's contribution to the formalization of mathematics
Indagationes Mathematicae, Vol. 24 (4), Special issue: In memory of N.G. (Dick) de Bruijn (1918-2012), pp. 1034-1049.
Elsevier, 2013 |
| 2012 |
Francien Dechesne, Rob Nederpelt
N.G. de Bruijn (1918-2012) and his Road to Automath, the Earliest Proof Checker
The Mathematical Intelligencer, Vol. 34 (1), Winter 2012, pp. 4-11.
Springer, 2012 |
| |
Fairouz Kamareddine, Twan Laan, Rob Nederpelt
A History of Types
Handbook of the History of Logic, Vol. 11 of the series Logic: A History of Its Central Concepts,
eds.: Dov M. Gabbay, Francis Jeffry Pelletier, and John Woods, pp. 451-511.
North Holland, 2012 |
| 2004 |
Gueorgui Jojgov, Rob Nederpelt
A Path to Faithful Formalizations of Mathematics
Proceedings of MKM Symposium 2004 (Mathematical Knowledge Management,
Third International Conference, Bialoweza, Poland).
Eds.: Andrea Asperti, Grzegorz Bancerek and Andrzej Trybulec.
Lecture Notes in Computer Science 3119, pp. 145-159.
Springer, 2004
|
| |
Herman Geuvers, Rob Nederpelt
Rewriting for Fitch style natural deductions
Proceedings of RTA 2004 (15th Internat. Conference on Rewriting
Techniques and Applications, Aachen, Germany).
Ed.: Vincent van Oostrom.
Lecture Notes in Computer Science 3091, pp. 134-154.
Springer, 2004 |
| |
G.I. Jojgov, R.P. Nederpelt, M. Scheffer
Faithfully reflecting the structure of informal mathematical
proofs into formal type theories
Proceedings of MKM Symposium 2003 (Mathematical Knowledge Management,
Heriot-Watt University, Scotland).
Ed.: Fairouz Kamareddine.
Electronic Notes in Theoretical Computer Science, Vol. 93,
pp. 102-117, 2004.
|
| |
Fairouz Kamareddine and Rob Nederpelt
A refinement of de Bruijn's formal language of mathematics.
Logic, Language and Information, Vol. 13 (3),
pp. 287-340.
Kluwer Academic Publishers, 2004 |
| 2003 |
Fairouz Kamareddine, Twan Laan and Rob Nederpelt:
Revisiting the notion of function.
Journal of Logic and Algebraic Programming, Vol.
54 (1-2), pp. 65-107, January 2003. Elsevier, North-Holland. |
| |
Fairouz Kamareddine, Twan Laan and Rob Nederpelt:
De Bruijn's
Automath and Pure Type Systems.
In: Fairouz Kamareddine, ed., Thirty Five Years of Automating
Mathematics, Kluwer Applied Logic series, Vol. 28, pp. 71-123.
Kluwer Academic Publishers, November 2003. |
| |
Fairouz Kamareddine, Twan Laan and Rob Nederpelt:
Automath and Pure Type Systems.
Electronic Notes in Theoretical Computer Science
85.7, 20 pp., Elsevier, 2003. |
| 2002 |
Fairouz Kamareddine, Twan Laan, Rob Nederpelt:
Types in Logic and Mathematics before 1940.
The Bulletin of Symbolic Logic, Vol. 8,
Number 2, June 2002, pp. 185-245. |
| |
Fairouz Kamareddine, Twan Laan and Rob Nederpelt:
Revisiting the notion of function,
Journal of Logic and
Algebraic Programming,
Volume 54, issue 1-2, Pages 65-107, December 2002. ISSN: 1567-8326.
Elsevier, North-Holland. |
| |
Tijn Borghuis, Fairouz Kamareddine and Rob Nederpelt:
Formalising belief revision in type theory,
The Logic
Journal of the Interest Group of Pure and Applied Logic ( Log.
J. IGPL),
Volume 10, issue 5, Pages 461-500, September 2002, ISSN 1367-0751,
Oxford University Press. |
| |
Roel Bloo, Fairouz Kamareddine, Twan Laan and Rob Nederpelt:
Parameters in Pure Type Systems,
Lecture Notes in Computer
Science 2286 (Latin American Theoretical Informatics, Latin 2002),
Pages 371-385, Rajsbaum, S., (Ed.), ISBN: 3-540-43400-3, Springer-Verlag,
March 2002. |
| 2001 |
Tijn Borghuis, Fairouz Kamareddine, Rob Nederpelt:
Belief Revision with Explicit Justifications: An Exploration in Type
Theory.
In: Intelligent Agent Technology: Research and Development,
World Scientific Publishers (The Second Asia-Pacific Conference on
Intelligent Agent Technology (IAT-2001),
October 2001, Maebashi City, Japan). |
| |
Fairouz Kamareddine, Roel Bloo, Rob Nederpelt:
De Bruijn's syntax and reductional equivalence of lambda-terms.
In: Proceedings Third International Conference on Principles and
Practice of Declarative Programming (PPDP01),
September 2001, Florence, Italy. |
| |
Rob Nederpelt, Fairouz Kamareddine:
An abstract syntax for a formal language of mathematics.
To be published in Proceedings Fourth International Tbilisi Symposium
on Language, Logic and Computation,
September 2001, Borjomi, Georgia. |
| |
Fairouz Kamareddine, Twan Laan, Rob Nederpelt:
Refining the Barendregt Cube using Parameters.
Lecture
Notes in Computer Science 2024,
2001 (Proceedings Fifth International Symposium on Functional and
Logic Programming (FLOPS 2001), Tokyo, Japan). |
| 1999 |
Fairouz Kamareddine, Roel Bloo, Rob Nederpelt:
On Pi-conversion in the lambda-cube and the combination with abbreviations.
Annals of Pure and Applied Logic 97,
1999, pp. 27-45. |
| 1998 |
Lex Bijlsma, Rob Nederpelt:
Dijkstra-Scholten predicate calculus: concepts and misconceptions.
Acta Informatica 35,
1998, pp. 1007-1036. |
| 1996 |
Twan Laan, Rob Nederpelt:
A Modern Elaboration of the Ramified Theory of Types.
Studia
Logica 57,
1996, pp. 243-278. |
| |
Fairouz Kamareddine, Rob Nederpelt:
Canonical typing and Pi-conversion in the Barendregt Cube.
Journal of Functional Programming 6 (2),
1996, pp. 245-267. |
| |
Roel Bloo, Fairouz Kamareddine and Rob Nederpelt:
The Barendregt Cube with Definitions and Generalised Reduction.
Information and Computation 126 (2),
1996, pp. 123-143. |
| |
Fairouz Kamareddine, Rob Nederpelt:
A useful lambda-notation.
Theoretical Computer Science
155 (1),
1996, pp. 85-109. |
| 1995 |
Fairouz Kamareddine, Rob Nederpelt:
Refining reduction in the lambda calculus.
Journal of
Functional Programming 5 (4),
1995, pp. 637-651. |
| 1994 |
R.P. Nederpelt, J.H. Geuvers:
Twenty-five years of Automath research.
In: Selected Papers on Automath (see above),
1994, pp. 3-54. |
| |
R.P. Nederpelt:
Type systems -- basic ideas and applications.
In: Selected Papers on Automath (see above),
1994, pp. 229-247. |
| |
R.P. Nederpelt:
Strong normalization in a typed lambda calculus with lambda structured
types.
In: Selected Papers on Automath (see above),
1994, pp. 389-468. |
| |
Fairouz Kamareddine, Rob Nederpelt:
A unified approach to type theory through a refined lambda-calculus.
Theoretical Computer Science 136,
1994, pp. 183-216. |
| 1993 |
Fairouz Kamareddine, Rob Nederpelt:
On stepwise explicit substitution.
International Journal
of Foundations of Computer Science Vol. 4, no. 3,
1993, pp. 197-240. |
| 1992 |
H.C.M. de Swart, R.P. Nederpelt:
Implication -- A Survey of the Different Logical Analyses of 'if ...,
then ...".
Nieuw Archief voor Wiskunde, vierde serie,
deel 10 (1, 2),
1992, pp. 77-103. |
Reports:
| 2002 |
Rob Nederpelt:
Weak Type Theory: A formal language for mathematics.
Computing Science Report 02-05,
Eindhoven University of Technology, Department of Math. and Comp.
Sc., May 2002. |
| 2000 |
Fairouz Kamareddine, Roel Bloo, Rob Nederpelt:
Characterizing lambda-terms with equal reduction behaviour.
Computing Science Reports 00-16,
Eindhoven University of Technology, Department of Math. and Comp.
Sc., October 2000. |
| |
Tijn Borghuis, Rob Nederpelt:
Belief Revision with Explicit Justifications.
Computing Science Report 00-17,
Eindhoven University of Technology, Department of Math. and Comp.
Sc., October 2000. |
| |
Twan Laan, Roel Bloo, Fairouz Kamareddine, Rob Nederpelt: Parameters
in Pure Type Systems.
Computing Science Reports 00-18,
Eindhoven University of Technology, Department of Math. and Comp.
Sc., November 2000. |
| 1994 |
R. Bloo, F. Kamareddine and R. Nederpelt:
On Pi-conversion in Type Theory.
Computing Science Reports 1994-47,
Eindhoven University of Technology, Department of Math. and Comp.
Sc., October 1994. |
| |
R. Bloo, F. Kamareddine and R. Nederpelt:
The lambda-cube with classes of terms modulo conversion.
Computing Science Reports 1994-46,
Eindhoven University of Technology, Department of Math. and Comp.
Sc., October 1994. |
| |
F. Kamareddine and R. Nederpelt:
Canonical typing and Pi-Conversion in the Barendregt Cube.
Computing Science Reports 94-36,
Eindhoven University of Technology, Department of Math. and Comp.
Sc., September 1994. |
| |
R. Bloo, F. Kamareddine and R. Nederpelt:
The Barendregt Cube with Definitions and Generalised Reduction.
Computing Science Reports 94-34,
Eindhoven University of Technology, Department of Math. and Comp.
Sc., September 1994. |
| |
R. Bloo, F. Kamareddine and R. Nederpelt:
Beyond beta-reduction in Church's lambda-arrow.
Computing Science Reports 94-20,
Eindhoven University of Technology, Department of Math. and Comp.
Sc., April 1994. |
| |
Fairouz Kamareddine, Rob Nederpelt:
Refining Reduction in the lambda calculus.
Departmental Research Report FM-94-03,
University of Glasgow, Dept. of Computing Science, April 1994.
Also published as: Computing Science Notes 94/18,
Eindhoven University of Technology, Department of Math. and Comp.
Sc., April 1994. |
| |
P. America, M. van der Kammen, R.P. Nederpelt and O.S. van Roosmalen:
The object-oriented paradigm.
Computing Science Notes 94/01,
Eindhoven University of Technology, Department of Math. and Comp.
Sc., January 1994. |
| |
Fairouz Kamareddine, Rob Nederpelt:
Canonical typing and Pi-Conversion.
Computing Science Research Report FM-93-10,
University of Glasgow, Dept. of Computing Science, October 1993.
Also published as: Computing Science Notes 94/02,
Eindhoven University of Technology, Department of Math. and Comp.
Sc., January 1994. |
| 1993 |
Fairouz Kamareddine, Rob Nederpelt:
A Semantics for a fine lambda-calculus with de Bruijn Indices.
Computing Science Research Report FM-93-9,
University of Glasgow, Dept. of Computing Science, September 1993.
Also published as: Computing Science Notes 93/28,
Eindhoven University of Technology, Department of Math. and Comp.
Sc., September 1993. |
| 1992 |
Fairouz Kamareddine, Rob Nederpelt:
On Stepwise Explicit Substitution.
Computing Science Research Report FM-1993-5,
University of Glasgow, Dept. of Computing Science, June 1993.
Also published as: Computing Science Notes 92/08,
Eindhoven University of Technology, Department of Math. and Comp.
Sc., April 1992. |
| |
Fairouz Kamareddine, Rob Nederpelt:
A Unified Approach to Type Theory Through a Refined Lambda-calculus.
Computing Science Research Report FM-1993-4,
University of Glasgow, Dept. of Computing Science, June 1993.
Also published as: Computing Science Notes 92/18,
Eindhoven University of Technology, Department of Math. and Comp.
Sc., September 1992. |
| |
R.P. Nederpelt:
The fine-structure of lambda calculus.
Computing Science Notes 92/07,
Eindhoven University of Technology, Department of Math. and Comp.
Sc., April 1992. |
|
