Mechanizing logical relations

Allen Stoughton

In Stephen Brookes et al., editors, Mathematical Foundations of Programming Semantics: 9th International Conference proceedings (New Orleans, LA, USA, 1993, April 7--10), number 802 in Lecture Notes in Computer Science, pages 359--377, Berlin, 1994. Springer-Verlag
Corrected version

Available as PostScript.

Abstract:

We give an algorithm for deciding whether there exists a definable element of a finite model of an applied typed lambda calculus that passes certain tests, in the special case when all the constants and test arguments are of order at most one. When there is such an element, the algorithm outputs a term that passes the tests; otherwise, the algorithm out puts a logical relation that demonstrates the nonexistence of such an element. Several example applications of the C implementation of this algorithm are considered.

Comments:
ISBN: 3-540-58027-1 / 0-387-58027-1

Authors address: Department of Computing and Information Sciences, Kansas State University, Manhattan, KS 66506, USA. E-mail:allen@cis.ksu.edu.

BRICS WWW home page