Jaber, Guilhem; Lewertowski, Gabriel; Pédrot, Pierre-Marie; Sozeau, Matthieu; Tabareau, Nicolas The definitional side of the forcing. (English) Zbl 1394.68063 Proceedings of the 2016 31st annual ACM/IEEE symposium on logic in computer science, LICS 2016, New York City, NY, USA, July 5–8, 2016. New York, NY: Association for Computing Machinery (ACM) (ISBN 978-1-4503-4391-6). 367-376 (2016). Cited in 3 Documents MSC: 68N18 Functional programming and lambda calculus 03B40 Combinatory logic and lambda calculus 03E40 Other aspects of forcing and Boolean-valued models 03G30 Categorical logic, topoi 68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) 68T15 Theorem proving (deduction, resolution, etc.) (MSC2010) Keywords:Coq; dependent type theory; effects; forcing; inductive types Citations:Zbl 1206.03017; Zbl 1364.03016 Software:Coq PDFBibTeX XMLCite \textit{G. Jaber} et al., in: Proceedings of the 2016 31st annual ACM/IEEE symposium on logic in computer science, LICS 2016, New York City, NY, USA, July 5--8, 2016. New York, NY: Association for Computing Machinery (ACM). 367--376 (2016; Zbl 1394.68063) Full Text: DOI HAL