The definitional side of the forcing

DOI10.1145/2933575.2935320MaRDI QIDQ4635893zbMATHOpenAlexFDO

Authors Guilhem Jaber, Gabriel Lewertowski, Pierre-Marie Pédrot, Matthieu Sozeau, Nicolas Tabareau

Publication date 23 April 2018

Published in Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1145/2933575.2935320

zbMATH Keywords

effectsforcingCoqdependent type theoryinductive types

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Combinatory logic and lambda calculus (03B40) Other aspects of forcing and Boolean-valued models (03E40) Categorical logic, topoi (03G30) Functional programming and lambda calculus (68N18)

Recommendations

• Extending type theory with forcing
• A computational interpretation of forcing in type theory
• A note on forcing and type theory
• scientific article; zbMATH DE number 1497808
• Forcing in Proof Theory

Cited in

(9)

• Failure is not an option. An exceptional type theory
• Extending type theory with forcing
• Higher order functions and Brouwer's thesis
• A computational interpretation of forcing in type theory
• A well-known representation of monoids and its application to the function ‘vector reverse’
• An effectful way to eliminate addiction to dependence
• Forcing revisited
• scientific article; zbMATH DE number 4068858 (Why is no real title available?)
• The \textsc{MetaCoq} project

Describes a project that uses

Uses Software

• Coq

This page was built for publication: The definitional side of the forcing

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