The Definitional Side of the Forcing

DOI10.1145/2933575.2935320zbMath1394.68063OpenAlexW2411119043MaRDI QIDQ4635893

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

effectsforcinginductive typesCoqdependent type theory

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Categorical logic, topoi (03G30) 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)

Related Items (3)

A well-known representation of monoids and its application to the function ‘vector reverse’ ⋮ The \textsc{MetaCoq} project ⋮ Higher order functions and Brouwer’s thesis

Uses Software

• Coq

This page was built for publication: The Definitional Side of the Forcing