The Definitional Side of the Forcing

DOI10.1145/2933575.2935320zbMATH Open1394.68063OpenAlexW2411119043MaRDI QIDQ4635893FDOQ4635893

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

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)

Cited In (5)

• The \textsc{MetaCoq} project
• A well-known representation of monoids and its application to the function ‘vector reverse’
• Forcing revisited
• Higher order functions and Brouwer’s thesis
• 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)