Explicit substitutions for constructive necessity

DOI10.1007/BFB0055098MaRDI QIDQ4219051zbMATH OpenFDO

Authors Neil Ghani, Eike Ritter, Valeria de Paiva

Publication date 15 November 1998

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

Full work available at URL https://doi.org/10.1007/BFB0055098

zbMATH Keywords

\(\lambda\)-calculusbinding analysisconstructive necessityexecution of programs in stagesexplicit substitutionspartial evaluationS4 modal logicsyntactic properties

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Logic in computer science (03B70) Functional programming and lambda calculus (68N18)

Recommendations

• A Theory of Explicit Substitutions with Safe and Full Composition
• scientific article; zbMATH DE number 1500649
• Explicit substitutions for the -calculus
• scientific article; zbMATH DE number 1231474

Cited in

(11)

• Order-dual relational semantics for non-distributive propositional logics: a general framework
• Fibrational modal type theory
• Classical natural deduction for S4 modal logic
• Dual and axiomatic systems for constructive S4, a formally verified equivalence
• Intuitionistic hypothetical logic of proofs
• A modal analysis of staged computation
• Linear explicit substitutions
• Partial Applicative Theories and Explicit Substitutions
• The Rule of Existential Generalisation and Explicit Substitution
• Axiomatic and dual systems for constructive necessity, a formally verified equivalence
• A categorical normalization proof for the modal lambda-calculus

This page was built for publication: Explicit substitutions for constructive necessity

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