Partiality and its Mechanization

This web page is intended to become an entry point to the
work on a proper treatment of expressions like 1/0.
It is originated by several workshops on this topic.

By its nature this web page will always be under construction. Currently it is at a very early stage. If you want something to be added, please send an e-mail to Manfred Kerber, University of Birmingham, UK, M.Kerber@cs.bham.ac.uk.

Workshops, events:

• CADE-15 Workshop on the Mechanization of Partial Functions, 5 July 1998, Lindau, Germany.
• CADE-13 Workshop on the Mechanization of Partial Functions, 30 July 1996, Rutgers University, New Brunswick, NJ, USA

Researchers working on partiality:

• Rob Arthan, Lemma 1 Ltd., Reading, UK
  e-mail: rda@lemma-one.com.
• Jeremy Dawson, ANU, Canberra, Australia
  e-mail: Jeremy.Dawson@cs.anu.edu.au.
• Solomon Feferman, Stanford University, Department of Mathematics, Stanford, CA
  e-mail: sf@csli.stanford.edu.
• Jürgen Giesl, TU Darmstadt, Darmstadt, Germany
  e-mail: giesl@informatik.tu-darmstadt.de
• Ray Gumb, University of Massachusetts, Lowell, MA, USA
  e-mail: gumb@cs.uml.edu
• Manfred Kerber, The University of Birmingham, School of Computer Science, UK
  e-mail: M.Kerber@cs.bham.ac.uk.
• Michael Kohlhase, Universität des Saarlandes, Saarbrücken, Germany
  e-mail: kohlhase@ags.uni-sb.de.

Papers on partiality:

• Jeremy E. Dawson: Simulating Term-Rewriting in LPF and in Display Logic. pointers to source, dvi, and ps files
• Raymond D. Gumb and Karel Lambert: Definitions in Nonstrict Positive Free Logic. pointers to abstract, dvi, and ps files
• Solomon Feferman (e-mail: sf@csli.stanford.edu): Definedness. Lecture for mini-conference on Partial Functions and Programming: Foundational Questions. U.C. Irvine, 17 May 1995.
  PostScript (296k).
• Manfred Kerber and Michael Kohlhase: A Tableau Calculus for Partial Functions.
  PostScript (121k), BibTeX-Entry (2k)