Hostname: page-component-7b9c58cd5d-g9frx Total loading time: 0 Render date: 2025-03-15T05:19:02.940Z Has data issue: false hasContentIssue false

Polymorphic lemmas and definitions in $\lambda$Prolog and Twelf

Published online by Cambridge University Press:  06 January 2004

ANDREW W. APPEL
Affiliation:
Department of Computer Science, Princeton University, NJ, USA (e-mail: appel@princeton.edu)
AMY P. FELTY
Affiliation:
School of Information Technology and Engineering, University of Ottawa, Canada (e-mail: afelty@site.uottawa.ca)
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the ‘Save PDF’ action button.

$\lambda$Prolog is known to be well-suited for expressing and implementing logics and inference systems. We show that lemmas and definitions in such logics can be implemented with a great economy of expression. We encode a higher-order logic using an encoding that maps both terms and types of the object logic (higher-order logic) to terms of the metalanguage ($\lambda$Prolog). We discuss both the Terzo and Teyjus implementations of $\lambda$Prolog. We also encode the same logic in Twelf and compare the features of these two metalanguages for our purposes.

Type
Regular Papers
Copyright
© 2004 Cambridge University Press