CADE-13 Workshop on
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).
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.