The definitional side of the forcing
From MaRDI portal
Publication:4635893
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
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
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)