An environment machine for the λμ-calculus

DOI10.1017/S0960129598002667zbMath0918.03017MaRDI QIDQ4236202

Philippe de Groote

Publication date: 17 August 1999

Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)

zbMATH Keywords

functional programmingcontrol operatorsextension of \(\lambda\)-calculusenvironment machinetyped \(\lambda\mu\)-calculus

Mathematics Subject Classification ID

Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) General topics in the theory of software (68N01) Combinatory logic and lambda calculus (03B40)

Related Items

Normalization in the simply typed -calculus ⋮ Normalization proofs for the un-typed \(\mu\mu^\prime\)-calculus ⋮ The differential \(\lambda \mu\)-calculus ⋮ Programming and Proving with Classical Types ⋮ A syntactic correspondence between context-sensitive calculi and abstract machines ⋮ Böhm theorem and Böhm trees for the \(\varLambda \mu\)-calculus ⋮ The next 700 Krivine machines ⋮ A proof-theoretic foundation of abortive continuations ⋮ Classical natural deduction for S4 modal logic ⋮ An estimation for the lengths of reduction sequences of the $\lambda\mu\rho\theta$-calculus ⋮ A Third-Order Representation of the λμ-Calculus