Towards the Theory of Programming in Constructive Logic
Abstract elided by the publisher.
Related papers
- Logic Programming and Logarithmic Space APLAS 2014
- Heterogeneous Dynamic Logic: Provability Modulo Program Theories PLDI 2026
- Completeness and decidability of converse PDL in the constructive type theory of Coq CPP 2018
- Large model constructions for second-order ZF in dependent type theory CPP 2018
- SteelCore: an extensible concurrent separation logic for effectful dependently typed programs ICFP 2020
- Fully abstract models for effectful λ-calculi via category-theoretic logical relations POPL 2022
- A two-level logic perspective on (simultaneous) substitutions CPP 2018
- The theory of deadlock avoidance via discrete control POPL 2009