Polymorphic lemmas and definitions in \lambdaProlog and Twelf

DOI10.1017/S1471068403001698MaRDI QIDQ4819003zbMATH OpenOpenAlexWikidataFDO

Authors Andrew W. Appel, Amy P. Felty

Publication date 24 September 2004

Published in Theory and Practice of Logic Programming (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1017/s1471068403001698

zbMATH Keywords

theorem provingpolymorphismlogical frameworksproof-carrying codehigher-order logic programmingTwelfLambda Prolog

Mathematics Subject Classification ID

Logic programming (68N17) Functional programming and lambda calculus (68N18)

Recommendations

• Encoding a dependent-type λ-calculus in a logic programming language
• scientific article; zbMATH DE number 1692888
• scientific article; zbMATH DE number 4164201
• Proof Pearl: The Power of Higher-Order Encodings in the Logical Framework LF
• scientific article; zbMATH DE number 1303348

Cited in

(3)

• Mechanized metatheory revisited
• A proposal for broad spectrum proof certificates
• scientific article; zbMATH DE number 1692888 (Why is no real title available?)

This page was built for publication: Polymorphic lemmas and definitions in $\lambda$Prolog and Twelf

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4819003)