Polymorphic lemmas and definitions in Lambda Prolog and Twelf

Simple item page
dc.creatorAppel, Andrew W.
dc.creatorFelty, Amy P.
dc.date2004-03-09
dc.date.accessioned2026-07-07T03:20:59Z
dc.date.available2026-07-07T03:20:59Z
dc.descriptionLambda 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.
dc.identifierhttps://arxiv.org/abs/cs/0403010
dc.identifierhttp://arxiv.org/abs/cs/0403010
dc.identifierAndrew W. Appel and Amy P. Felty, Polymorphic Lemmas and Definitions in Lambda Prolog and Twelf, Theory and Practice of Logic Programming, 4(1&2):1-39, January & March 2004
dc.identifier.urihttp://salesiana.dossiersoluciones.com/handle/123456789/32029
dc.subjectLogic in Computer Science
dc.subjectProgramming Languages
dc.subjectF.3.1; D.2.4; I.2.3; D.1.6
dc.titlePolymorphic lemmas and definitions in Lambda Prolog and Twelf
dc.typetext

Files

Collections

arXiv