research
∙
01/04/2023
Proofs as stateful programs: A first-order logic with abstract Hoare triples, and an interpretation into an imperative language
We introduce an extension of first-order logic that comes equipped with ...
share
research
∙
01/10/2020
A computational interpretation of Zorn's lemma
We give a computational interpretation to an abstract instance of Zorn's...
research
∙
06/25/2019
A unifying framework for continuity and complexity in higher types
We set up a parametrised monadic translation for a class of call-by-valu...
research
∙
03/07/2019
An algorithmic approach to the existence of ideal objects in commutative algebra
The existence of ideal objects, such as maximal ideals in nonzero rings,...
research
∙
02/25/2019
Dependent choice as a termination principle
We introduce a new formulation of the axiom of dependent choice that can...
research
∙
12/28/2018
Sequential algorithms and the computational content of classical proofs
We develop a correspondence between the theory of sequential algorithms ...
research
∙
12/14/2018