The _-calculus

DOI10.1007/3-540-57887-0_113MaRDI QIDQ4490747zbMATH OpenFDO

Authors Niels Jakob Rehof, M. H. B. Sørensen

Publication date 20 July 2000

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

Full work available at URL https://doi.org/10.1007/3-540-57887-0_113

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Functional programming and lambda calculus (68N18)

Recommendations

• scientific article; zbMATH DE number 7340561
• A confluent λ-calculus with a catch/throw mechanism
• Explicit substitutions for the -calculus
• Strong normalizability of the non-deterministic catch/throw calculi
• A syntactic theory of sequential control

Cited in

(33)

• A syntactic theory of sequential control
• Intuitionistic and classical natural deduction systems with the catch and the throw rules
• A classical linear \(\lambda\)-calculus
• The polarized \(\lambda\)-calculus
• Non-strictly positive fixed points for classical natural deduction
• An interpretation of \(\lambda \mu\)-calculus in \(\lambda\)-calculus.
• The differential lambda-calculus
• Parametric parameter passing \(\lambda\)-calculus
• The differential \(\lambda \mu\)-calculus
• Domain-free -calculus
• Church's lambda delta calculus
• The formal system λδ
• Dualized simple type theory
• A simple calculus of exception handling
• scientific article; zbMATH DE number 4213958 (Why is no real title available?)
• Control reduction theories: the benefit of structural substitution
• Jumbo λ-Calculus
• Böhm theorem and Böhm trees for the \(\varLambda \mu\)-calculus
• The basis decision problem in λ‐calculus
• scientific article; zbMATH DE number 627411 (Why is no real title available?)
• Explicit substitutions for the -calculus
• Deriving a Floyd-Hoare logic for non-local jumps from a formulæ-as-types notion of control
• scientific article; zbMATH DE number 2063227 (Why is no real title available?)
• Formulae-as-types for an involutive negation
• A short proof of the strong normalization of classical natural deduction with disjunction
• An intuitionistic λ-calculus with exceptions
• scientific article; zbMATH DE number 837069 (Why is no real title available?)
• A confluent λ-calculus with a catch/throw mechanism
• scientific article; zbMATH DE number 1443050 (Why is no real title available?)
• Hereditary substitution for the \(\lambda \Delta \)-calculus
• A note on strong normalization in classical natural deduction
• Disjunctive normal forms and local exceptions
• Normalization in the simply typed -calculus

This page was built for publication: The \(\lambda_\Delta\)-calculus

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