The definitional side of the forcing

DOI10.1145/2933575.2935320zbMATH Open1394.68063OpenAlexW2411119043MaRDI QIDQ4635893FDOQ4635893

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

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

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)

Cited In (9)

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

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)