A Formal Correspondence Between OMDoc with Alternative Proofs and the {\overline{\lambda}\mu\tilde{\mu}} -Calculus

DOI10.1007/11812289_7MaRDI QIDQ5756760zbMATH OpenOpenAlexFDO

Authors Serge Autexier, Claudio Sacerdoti Coen

Publication date 5 September 2007

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

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

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Knowledge representation (68T30)

Recommendations

• On the formalization of the modal -calculus in the calculus of inductive constructions
• scientific article; zbMATH DE number 2174387
• The \(\lambda \)-calculus and the unity of structural proof theory
• On the proof theory of the modal mu-calculus
• Formal SOS-Proofs for the Lambda-Calculus
• Publication:4938644
• A note on the proof theory of the -calculus
• Algorithmic correspondence for intuitionistic modal mu-calculus
• Towards proof planning for \(\mathcal{M}_{\omega}^+\)
• Towards a formal proof system for \(\omega\)-rational expressions

Cited in

(3)

• Declarative representation of proof terms
• A Logically Saturated Extension of ${{\bar\lambda\mu\tilde{\mu}}}$
• Authoring Verified Documents by Interactive Proof Construction and Verification in Text-Editors

This page was built for publication: A Formal Correspondence Between OMDoc with Alternative Proofs and the ${\overline{\lambda}\mu\tilde{\mu}}$ -Calculus

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