| Publication | Date of Publication | Type |
|---|
Proof Pearl: faithful computation and extraction of \(\mu\)-recursive algorithms in Coq
| 2024-11-26 | Paper |
Internal and External Calculi: Ordering the Jungle without Being Lost in Translations
| 2023-12-06 | Paper |
Synthetic Undecidability of MSELL via FRACTRAN Mechanised in Coq
| 2023-06-23 | Paper |
Trakhtenbrot’s Theorem in Coq
Automated Reasoning | 2022-11-09 | Paper |
scientific article; zbMATH DE number 7566048 (Why is no real title available?)
| 2022-08-02 | Paper |
scientific article; zbMATH DE number 7566073 (Why is no real title available?)
| 2022-08-02 | Paper |
Hilbert's Tenth Problem in Coq
| 2022-07-18 | Paper |
The Braga Method: Extracting Certified Algorithms from Complex Recursive Schemes in Coq
Proof and Computation II | 2022-06-17 | Paper |
Trakhtenbrot's Theorem in Coq: Finite Model Theory through the Constructive Lens
| 2021-04-29 | Paper |
Constructive decision via redundancy-free proof-search
Journal of Automated Reasoning | 2020-11-02 | Paper |
Certification of breadth-first algorithms by extraction
| 2020-05-05 | Paper |
Trakhtenbrot's Theorem in Coq, A Constructive Approach to Finite Model Theory
| 2020-04-15 | Paper |
Constructive decision via redundancy-free proof-search
Automated Reasoning | 2018-10-18 | Paper |
Proof pearl: constructive extraction of cycle finding algorithms
| 2018-10-04 | Paper |
Typing total recursive functions in Coq
| 2018-01-04 | Paper |
Separation logic with one quantified variable
Theory of Computing Systems | 2017-10-20 | Paper |
An Alternative Direct Simulation of Minsky Machines into Classical Bunched Logics via Group Semantics
Electronic Notes in Theoretical Computer Science | 2016-07-08 | Paper |
The formal strong completeness of partial monoidal Boolean BI
Journal Of Logic And Computation | 2016-07-07 | Paper |
Nondeterministic phase semantics and the undecidability of Boolean BI
ACM Transactions on Computational Logic | 2015-09-17 | Paper |
Looking at separation algebras with Boolean BI-eyes
Advanced Information Systems Engineering | 2014-09-15 | Paper |
Separation logic with one quantified variable
Computer Science - Theory and Applications | 2014-06-24 | Paper |
Gödel-Dummett counter-models through matrix computation
| 2013-09-25 | Paper |
Some remarks on relations between proofs and games
| 2011-06-21 | Paper |
Exploring the relation between Intuitionistic BI and Boolean BI: an unexpected embedding
Mathematical Structures in Computer Science | 2009-06-30 | Paper |
Bounding Resource Consumption with Gödel-Dummett Logics
Logic for Programming, Artificial Intelligence, and Reasoning | 2008-05-27 | Paper |
Expressivity Properties of Boolean BI Through Relational Models
FSTTCS 2006: Foundations of Software Technology and Theoretical Computer Science | 2008-04-17 | Paper |
Automated Reasoning
Lecture Notes in Computer Science | 2007-09-25 | Paper |
Graph-based decision for Gödel-Dummett logics
Journal of Automated Reasoning | 2007-05-04 | Paper |
scientific article; zbMATH DE number 2090290 (Why is no real title available?)
| 2004-08-12 | Paper |
scientific article; zbMATH DE number 1770113 (Why is no real title available?)
| 2002-07-22 | Paper |
scientific article; zbMATH DE number 1531367 (Why is no real title available?)
| 2001-02-28 | Paper |
scientific article; zbMATH DE number 1500555 (Why is no real title available?)
| 2001-01-14 | Paper |
scientific article; zbMATH DE number 1231699 (Why is no real title available?)
| 1999-01-10 | Paper |
