Mechanizing logical relations
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
Available as PostScript.
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.
ISBN: 3-540-58027-1 / 0-387-58027-1
address: Department of Computing and Information Sciences, Kansas State
University, Manhattan, KS 66506, USA. E-mail:email@example.com.
BRICS WWW home page