17 citations · 24 across the 8 of their papers we have counts for
4 papers · 1 filter
Verified completeness in Henkin-style for intuitionistic propositional logic
Huayu Guo, Dongheng Chen, Bruno Bentzen
This paper presents a formalization of the classical proof of completeness in Henkin-style developed by Troelstra and van Dalen for intuitionistic logic with respect to Kripke mode…
Naive cubical type theory
Bruno Bentzen
This paper proposes a way of doing type theory informally, assuming a cubical style of reasoning. It can thus be viewed as a first step toward a cubical alternative to the program…
A Henkin-style completeness proof for the modal logic S5
Bruno Bentzen
This paper presents a recent formalization of a Henkin-style completeness proof for the propositional modal logic S5 using the Lean theorem prover. The proof formalized is close to…
Cubical informal type theory: the higher groupoid structure
Bruno Bentzen
Following a project of developing conventions and notations for informal type theory carried out in the homotopy type theory book for a framework built out of an augmentation of co…