/ W&I - Rob NederpeltTU/e - Computing Science dep. / zoek / reageer
 

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:

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.

Rob Nederpelt

contact
publications
links
book Type Theory