A λprolog based animation of twelf specifications

Mary K Southern, Gopalan Nadathur

Research output: Contribution to conferencePaper

1 Scopus citations

Abstract

Specifications in the Twelf system are based on a logic programming interpretation of the Edinburgh Logical Framework or LF. We consider an approach to animating such specifications using a λProlog implementation. This approach is based on a lossy translation of the dependently typed LF expressions into the simply typed lambda calculus (STLC) terms of λProlog and a subsequent encoding of lost dependency information in predicates that are defined by suitable clauses. To use this idea in an implementation of logic programming a la Twelf, it is also necessary to translate the results found for λProlog queries back into LF expressions. We describe such an inverse translation and show that it has the necessary properties to facilitate an emulation of Twelf behavior through our translation of LF specifications into λProlog programs. A characteristic of Twelf is that it permits queries to consist of types which have unspecified parts represented by meta-variables for which values are to be found through computation. We show that this capability can be supported within our translation based approach to animating Twelf specifications.

Original languageEnglish (US)
Pages63-78
Number of pages16
StatePublished - Jun 1 2014
EventInternational Joint Workshop on Implementation of Constraint and Logic Programming Systems and Logic-Based Methods in Programming Environments 2014, CICLOPS-WLPE 2014 - Vienna, Austria
Duration: Jul 17 2014Jul 18 2014

Other

OtherInternational Joint Workshop on Implementation of Constraint and Logic Programming Systems and Logic-Based Methods in Programming Environments 2014, CICLOPS-WLPE 2014
CountryAustria
CityVienna
Period7/17/147/18/14

Fingerprint Dive into the research topics of 'A λprolog based animation of twelf specifications'. Together they form a unique fingerprint.

  • Cite this

    Southern, M. K., & Nadathur, G. (2014). A λprolog based animation of twelf specifications. 63-78. Paper presented at International Joint Workshop on Implementation of Constraint and Logic Programming Systems and Logic-Based Methods in Programming Environments 2014, CICLOPS-WLPE 2014, Vienna, Austria.