Tradeoffs in the intensional representation of lambda terms

DOI10.1007/3-540-45610-4_14MaRDI QIDQ4808747zbMATH OpenFDO

Authors Chuck Liang, Gopalan Nadathur

Publication date 12 August 2004

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL http://link.springer.de/link/service/series/0558/bibs/2378/23780192.htm

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• Choices in representation and reduction strategies for lambda terms in intensional contexts
• scientific article; zbMATH DE number 1332647
• A notation for lambda terms. A generalization of environments
• The suspension notation for lambda terms and its use in metalanguage implementations
• de Bruijn notation as a nested datatype

Cited in

(5)

• Comparing and implementing calculi of explicit substitutions with eta-reduction
• Why Would You Trust B?
• The suspension notation for lambda terms and its use in metalanguage implementations
• Logical Aspects of Computational Linguistics
• Choices in representation and reduction strategies for lambda terms in intensional contexts

Describes a project that uses

Uses Software

• Coq
• Nuprl

This page was built for publication: Tradeoffs in the intensional representation of lambda terms

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