Many practical applications of deduction systems in mathematics and computer science rely on the correct and efficient treatment of partial functions. There is a rich variety of approaches for dealing with partial functions and the undefined expressions that often result from their application. Ranging from workarounds for concrete situations to proper general treatments, these approaches have their own advantages and disadvantages. For example, some can be used in standard logical formalisms, while others require new formalisms. The purpose of the workshop is to discuss the different approaches and to compare their advantages and disadvantages.

Potential participants can apply by submitting a short statement that contains a description of their current interests by e-mail to Manfred Kerber at M.Kerber@cs.bham.ac.uk.
The original Call for Participation can be found here.

Those invited to attend the workshop have to register for the workshop in conjunction with the CADE main conference. Registration and travel information can be found in the general information of FLoC'96 (Federated Logic Conference).

Organizers:

• William Farmer, The MITRE Corporation, USA, farmer@mitre.org
• Manfred Kerber, The University of Birmingham, UK, M.Kerber@cs.bham.ac.uk
• Michael Kohlhase, Uni des Saarlandes, Germany, kohlhase@cs.uni-sb.de

 9:00 -  9:05  Opening Remarks: W. Farmer

 9:05 - 10:15  Invited Address
               
               R. Constable 
	       "Reasoning about Partial Functions in Type Theory" 
               (PostScript Abstract, compressed 8k)

10:15 - 10:30  Break

10:30 - 12:15  Session I
               Chair: M. Kohlhase

               C. Jones, "TANSTAAFL (with partial functions)"
               (PostScript, compressed 42k)

	       J. Giesl, "Proving partial correctness of partial
               functions"
               (PostScript, compressed 31k)

               O. Müller*, K. Slind, "Isabelle/HOL as a Platform for
               Partiality"
               (PostScript, compressed 47k)

               R. Gumb*, K. Lambert, "A free logical foundation for
               nonstrict functions"
               (PostScript, compressed 40k)

               M. Kerber*, M. Kohlhase, "Partiality without the cost"
               (PostScript, compressed 49k)

               Discussion

12:15 - 13:45  Lunch Break

13:45 - 15:00  Session II
               Chair: W. Farmer

               W. Maurer, "The use of partial functions in proving
               that a program does not crash"
               (PostScript, compressed 44k)

               A. Yakhnis, V. Yakhnis*, V. Winter, "Software with Partial Functions: 
               Automating Correctness Proofs via Nonstrict Explicit Domains"
               (PostScript, compressed 1297k)

               J. Avenhaus*, K. Madlener, "Partial Functions in
               Clausal Specifications"
               (PostScript, compressed 106k)

               Discussion

15:00 - 15:15  Break

15:15 - 16:30  Session III
               Chair: M. Kerber

               R. Arthan, "Undefinedness in Z: Issues for
               specification and proof"
               (PostScript, compressed 124k)

               W. Farmer, "Mechanizing the traditional approach to
               partial functions"
               (PostScript, compressed 56k)

               E. Gunter, "Partial functions as total functions"
               (PostScript, compressed 38k)

               Discussion

16:30 - 17:00  Panel Discussion on Approaches
               Chair: M. Kohlhase

               Panel members: R. Arthan, R. Constable, W. Farmer, C. Jones

* Presenter
The cover sheet and table of contents of the workshop proceedings can be found here,
PostScript, compressed 32k.