| Publication | Date of Publication | Type |
|---|
Program extraction from classical proofs
Lecture Notes in Computer Science | 2023-12-12 | Paper |
| scientific article; zbMATH DE number 7731929 (Why is no real title available?) | 2023-08-26 | Paper |
On the Computational Content of Choice Principles
Handbook of Constructive Mathematics | 2023-08-11 | Paper |
Concurrent Gaussian Elimination
Mathematics for Computation (M4C) | 2023-08-04 | Paper |
Extracting total Amb programs from proofs
Programming Languages and Systems | 2023-08-03 | Paper |
| \textsc{Prawf}: an interactive proof system for program extraction | 2022-12-16 | Paper |
| Martin Hofmann's Case for Non-Strictly Positive Data Types | 2022-07-21 | Paper |
Intuitionistic fixed point logic
Annals of Pure and Applied Logic | 2021-01-25 | Paper |
Logic for Gray-code computation
Concepts of Proof in Mathematics, Philosophy, and Computer Science | 2020-04-03 | Paper |
Program extraction applied to monadic parsing
Journal Of Logic And Computation | 2019-07-29 | Paper |
The greatest common divisor: A case study for program extraction from classical proofs
Lecture Notes in Computer Science | 2019-01-15 | Paper |
| Undecidability of equality for codata types | 2018-10-23 | Paper |
| Optimized program extraction for induction and coinduction | 2018-09-06 | Paper |
A realizability interpretation of Church's simple theory of types
Mathematical Structures in Computer Science | 2017-11-22 | Paper |
A coinductive approach to computing with compact sets
Journal of Logic and Analysis | 2017-04-10 | Paper |
| Extracting imperative programs from proofs: In-place Quicksort | 2017-03-13 | Paper |
Typed vs. untyped realizability
Electronic Notes in Theoretical Computer Science | 2016-07-08 | Paper |
Extracting a DPLL algorithm
Electronic Notes in Theoretical Computer Science | 2016-07-08 | Paper |
Extracting verified decision procedures: DPLL and resolution
Logical Methods in Computer Science | 2015-03-11 | Paper |
Uniform schemata for proof rules
Language, Life, Limits | 2015-02-25 | Paper |
Proofs, programs, processes
Theory of Computing Systems | 2012-12-07 | Paper |
| Realisability and adequacy for (co)induction | 2012-09-28 | Paper |
Minlog -- a tool for program extraction supporting algebras and coalgebras
Algebra and Coalgebra in Computer Science | 2011-09-02 | Paper |
From coinductive proofs to exact real arithmetic: theory and applications
Logical Methods in Computer Science | 2011-05-26 | Paper |
| Program extraction via typed realisability for induction and coinduction | 2011-03-09 | Paper |
| Realisability for induction and coinduction with applications to constructive analysis | 2011-02-10 | Paper |
Proofs, programs, processes
Programs, Proofs, Processes | 2010-07-29 | Paper |
Domain representations of spaces of compact subsets
Mathematical Structures in Computer Science | 2010-05-17 | Paper |
From Coinductive Proofs to Exact Real Arithmetic
Computer Science Logic | 2009-11-12 | Paper |
Coinduction for exact real number computation
Theory of Computing Systems | 2009-05-08 | Paper |
A provably correct translation of the \(\lambda \)-calculus into a mathematical model of C++
Theory of Computing Systems | 2009-05-08 | Paper |
A domain model characterising strong normalisation
Annals of Pure and Applied Logic | 2008-12-05 | Paper |
Classical truth in higher types
Mathematical Logic Quarterly | 2008-06-12 | Paper |
Strong normalisation for applied lambda calculi
Logical Methods in Computer Science | 2007-10-11 | Paper |
Continuous semantics for strong normalisation
Mathematical Structures in Computer Science | 2007-02-09 | Paper |
Computer Science Logic
Lecture Notes in Computer Science | 2006-11-01 | Paper |
Modified bar recursion
Mathematical Structures in Computer Science | 2006-08-10 | Paper |
Program extraction from normalization proofs
Studia Logica | 2006-03-17 | Paper |
| scientific article; zbMATH DE number 2247255 (Why is no real title available?) | 2006-01-16 | Paper |
New Computational Paradigms
Lecture Notes in Computer Science | 2006-01-11 | Paper |
| scientific article; zbMATH DE number 2222013 (Why is no real title available?) | 2005-11-02 | Paper |
Uniform Heyting arithmetic
Annals of Pure and Applied Logic | 2005-04-21 | Paper |
An arithmetic for non-size-increasing polynomial-time computation
Theoretical Computer Science | 2004-08-06 | Paper |
| scientific article; zbMATH DE number 2006631 (Why is no real title available?) | 2003-11-23 | Paper |
| scientific article; zbMATH DE number 1984266 (Why is no real title available?) | 2003-09-22 | Paper |
Term rewriting for normalization by evaluation.
Information and Computation | 2003-08-19 | Paper |
| scientific article; zbMATH DE number 1552509 (Why is no real title available?) | 2003-07-29 | Paper |
Computability and totality in domains
Mathematical Structures in Computer Science | 2002-10-31 | Paper |
Refined program extraction from classical proofs
Annals of Pure and Applied Logic | 2002-09-16 | Paper |
| scientific article; zbMATH DE number 1497739 (Why is no real title available?) | 2001-03-06 | Paper |
The Warshall algorithm and Dickson's lemma: Two examples of realistic program extraction
Journal of Automated Reasoning | 2001-02-18 | Paper |
| scientific article; zbMATH DE number 1405571 (Why is no real title available?) | 2000-02-23 | Paper |
Density theorems for the domains-with-totality semantics of dependent types
Applied Categorical Structures | 1999-11-29 | Paper |
| scientific article; zbMATH DE number 956826 (Why is no real title available?) | 1997-07-01 | Paper |
| scientific article; zbMATH DE number 895269 (Why is no real title available?) | 1996-07-01 | Paper |
| scientific article; zbMATH DE number 785043 (Why is no real title available?) | 1995-09-26 | Paper |
| scientific article; zbMATH DE number 512774 (Why is no real title available?) | 1994-05-15 | Paper |
Total sets and objects in domain theory
Annals of Pure and Applied Logic | 1993-05-16 | Paper |
| scientific article; zbMATH DE number 4212032 (Why is no real title available?) | 1990-01-01 | Paper |
