Hostname: page-component-cd9895bd7-8ctnn Total loading time: 0 Render date: 2024-12-24T16:23:02.731Z Has data issue: false hasContentIssue false
  • English
  • Français

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

Published online by Cambridge University Press:  06 January 2004

ANDREW W. APPEL  and
AMY P. FELTY
ANDREW W. APPEL
Affiliation:
Department of Computer Science, Princeton University, NJ, USA (e-mail: [email protected])
AMY P. FELTY
Affiliation:
School of Information Technology and Engineering, University of Ottawa, Canada (e-mail: [email protected])
Get access Rights & Permissions [Opens in a new window]

Abstract

$\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
Information
Theory and Practice of Logic Programming , Volume 4 , Issue 1-2 , January 2004 , pp. 1 - 39
Copyright
© 2004 Cambridge University Press

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)