CFP CADE-Workshop Partiality

Updated Call for Participation

CADE-13 Workshop on

Mechanization of Partial Functions

30 July 1996 Rutgers University, New Brunswick, NJ, USA

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
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).


The workshop schedule is:
 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
               (PostScript, compressed 31k)

               O. Müller*, K. Slind, "Isabelle/HOL as a Platform for
               (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)


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)


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)


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.

last updated: 5 July 1996