Functional runtime systems within the lambda-sigma calculus

DOI10.1017/S0956796898002986zbMATH Open0918.03018OpenAlexW2160740215MaRDI QIDQ4236754FDOQ4236754

Authors Thérèse Hardin, Luc Maranget, Bruno Pagano

Publication date 17 August 1999

Published in Journal of Functional Programming (Search for Journal in Brave)

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

zbMATH Keywords

abstract machinesKrivine machineruntime systemsCAMFAMfunctional compilersSECDweak \(\lambda\)-calculus

Mathematics Subject Classification ID

Theory of compilers and interpreters (68N20) Specification and verification (program logics, model checking, etc.) (68Q60) Combinatory logic and lambda calculus (03B40) Logic in computer science (03B70)

Recommendations

• Functional back-ends within the lambda-sigma calculus
• A Theory of Explicit Substitutions with Safe and Full Composition
• Explaining the lazy Krivine machine using explicit substitution and addresses
• scientific article; zbMATH DE number 2079040
• Strong normalization of substitutions

Cited in

(16)

• Coinductive big-step operational semantics
• Sequent calculus as a compiler intermediate language
• Strongly reducing variants of the Krivine abstract machine
• A functional correspondence between call-by-need evaluators and lazy abstract machines
• Comparing calculi of explicit substitutions with eta-reduction
• From reduction-based to reduction-free normalization
• State-transition machines for lambda-calculus expressions
• Lambda-calculus with director strings
• A provably correct translation of the \(\lambda \)-calculus into a mathematical model of C++
• A syntactic correspondence between context-sensitive calculi and abstract machines
• Explaining the lazy Krivine machine using explicit substitution and addresses
• A provably correct compilation of functional languages into scripting languages
• scientific article; zbMATH DE number 7204429 (Why is no real title available?)
• Inter-deriving semantic artifacts for object-oriented programming
• Comparing and implementing calculi of explicit substitutions with eta-reduction
• Functional back-ends within the lambda-sigma calculus

This page was built for publication: Functional runtime systems within the lambda-sigma calculus

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