Normalisation by completeness with Heyting algebras

DOI10.1007/978-3-662-48899-7_33MaRDI QIDQ3460077zbMATH OpenOpenAlexFDO

Authors Gaëtan Gilbert, Olivier Hermant

Publication date 12 January 2016

Published in Logic for Programming, Artificial Intelligence, and Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-662-48899-7_33

Mathematics Subject Classification ID

Subsystems of classical logic (including intuitionistic logic) (03B20) Cut-elimination and normal-form theorems (03F05) Heyting algebras (lattice-theoretic aspects) (06D20) Formalization of mathematics in connection with theorem provers (68V20)

Recommendations

• scientific article; zbMATH DE number 1757129
• Foundations of Software Science and Computation Structures
• Truth Values Algebras and Proof Normalization
• scientific article; zbMATH DE number 1101617
• Normalization by evaluation and algebraic effects

Cited in

(2)

• Truth Values Algebras and Proof Normalization
• Explicit Composition and Its Application in Proofs of Normalization

Describes a project that uses

Uses Software

• Coq

This page was built for publication: Normalisation by completeness with Heyting algebras

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