Vincent Rahli

List of research outcomes

This list is not complete and representing at the moment only items from zbMATH Open and arXiv. We are working on additional sources - please check back here soon!

Publication	Date of Publication	Type
Open bar -- a Brouwerian intuitionistic logic with a pinch of excluded middle	2026-03-23	Paper
Separating Markov's principles	2025-06-18	Paper
Inductive continuity via Brouwer trees	2024-12-03	Paper
Realizing continuity using stateful computations	2024-09-25	Paper
\(\text{TT}^\Box_{\mathcal{C}}\): a family of extensional type theories with effectful realizers of continuity Logical Methods in Computer Science	2024-09-04	Paper
Constructing unprejudiced extensional type theories with choices via modalities	2024-05-27	Paper
Computability beyond Church-Turing via choice sequences Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science	2021-01-20	Paper
Bar induction. The good, the bad, and the ugly	2021-01-19	Paper
Bar induction is compatible with constructive type theory Journal of the ACM	2019-11-21	Paper
A verified theorem prover backend supported by a monotonic library EPiC Series in Computing	2019-07-04	Paper
Validating Brouwer's continuity principle for numbers using named exceptions Mathematical Structures in Computer Science	2018-05-17	Paper
Skalpel: a constraint-based type error slicer for standard ML Journal of Symbolic Computation	2017-02-06	Paper
Exercising Nuprl's open-endedness Mathematical Software – ICMS 2016	2016-09-28	Paper
Skalpel: a type error slicer for standard ML	2016-08-01	Paper
Simplified reducibility proofs of Church-Rosser for \({\beta}\)- and \({\beta}{\eta}\)-reduction Electronic Notes in Theoretical Computer Science	2015-03-18	Paper
Towards a formally verified proof assistant Interactive Theorem Proving	2014-09-08	Paper
Formal program optimization in Nuprl using computational equivalence and partial types Interactive Theorem Proving	2013-08-07	Paper
On realisability semantics for intersection types with expansion variables Fundamenta Informaticae	2013-01-24	Paper
Reducibility Proofs in the λ-Calculus Fundamenta Informaticae	2013-01-24	Paper
Realisability Semantics for Intersection Types and Expansion Variables	2009-05-13	Paper
A Complete Realisability Semantics for Intersection Types and Arbitrary Expansion Variables Theoretical Aspects of Computing - ICTAC 2008	2009-01-27	Paper
Uniform Circuits, & Boolean Proof Nets Logical Foundations of Computer Science	2008-01-04	Paper

Research outcomes over time

This page was built for person: Vincent Rahli