| Publication | Date of Publication | Type |
|---|
Formal small-step verification of a call-by-value lambda calculus machine
Programming Languages and Systems | 2023-08-02 | Paper |
scientific article; zbMATH DE number 7699436 (Why is no real title available?)
| 2023-06-20 | Paper |
A foundation for higher-order concurrent constraint programming
Constraints in Computational Logics | 2022-08-16 | Paper |
A confluent relational calculus for higher-order programming with constraints
Constraints in Computational Logics | 2022-08-16 | Paper |
A record calculus with principal types
Constraints in Computational Logics | 2022-08-16 | Paper |
scientific article; zbMATH DE number 7204440 (Why is no real title available?)
| 2020-05-26 | Paper |
Call-by-value lambda calculus as a model of computation in Coq
Journal of Automated Reasoning | 2019-08-21 | Paper |
Categoricity results and large model constructions for second-order ZF in dependent type theory
Journal of Automated Reasoning | 2019-08-21 | Paper |
Verification of PCP-related computational reductions in Coq
| 2018-10-04 | Paper |
Regular language representations in the constructive type theory of Coq
Journal of Automated Reasoning | 2018-08-21 | Paper |
Weak call-by-value lambda calculus as a model of computation in Coq
| 2018-01-04 | Paper |
Categoricity results for second-order ZF in dependent type theory
| 2018-01-04 | Paper |
Tower induction and up-to techniques for CCS with fixed points
Relational and Algebraic Methods in Computer Science | 2017-07-21 | Paper |
Unification modulo nonnested recursion schemes via anchored semi-unification
| 2017-02-01 | Paper |
Two-Way Automata in Coq
Interactive Theorem Proving | 2016-10-27 | Paper |
Hereditarily finite sets in constructive type theory
Interactive Theorem Proving | 2016-10-27 | Paper |
Clausal tableaux for hybrid PDL
Electronic Notes in Theoretical Computer Science | 2016-10-07 | Paper |
Completeness and decidability results for CTL in constructive type theory
Journal of Automated Reasoning | 2016-05-26 | Paper |
Transfinite constructions in classical type theory
Interactive Theorem Proving | 2015-09-14 | Paper |
A linear first-order functional intermediate language for verified compilers
Interactive Theorem Proving | 2015-09-14 | Paper |
Autosubst: Reasoning with de Bruijn Terms and Parallel Substitutions
Interactive Theorem Proving | 2015-09-14 | Paper |
A goal-directed decision procedure for hybrid PDL
Journal of Automated Reasoning | 2015-06-23 | Paper |
Hybrid tableaux for the difference modality
Electronic Notes in Theoretical Computer Science | 2015-03-23 | Paper |
A constructive theory of regular languages in Coq
Certified Programs and Proofs | 2015-01-13 | Paper |
Completeness and Decidability Results for CTL in Coq
Interactive Theorem Proving | 2014-09-08 | Paper |
Higher-order syntax and saturation algorithms for hybrid logic
Electronic Notes in Theoretical Computer Science | 2013-12-20 | Paper |
Constructive completeness for modal logic with transitive closure
Certified Programs and Proofs | 2013-04-19 | Paper |
Programming -- an introduction to computer science with Standard ML
| 2011-12-02 | Paper |
Constructive Formalization of Hybrid Logic with Eventualities
Certified Programs and Proofs | 2011-11-22 | Paper |
Programming -- an introduction to computer science with Standard ML
| 2011-09-22 | Paper |
Correctness and worst-case optimality of Pratt-style decision procedures for modal and hybrid logics
Lecture Notes in Computer Science | 2011-07-01 | Paper |
Terminating tableaux for graded hybrid logic with global modalities and role hierarchies
Logical Methods in Computer Science | 2011-05-26 | Paper |
A finite axiomatization of propositional type theory in pure lambda calculus
| 2011-03-30 | Paper |
Terminating Tableaux for $\mathcal{SOQ}$ with Number Restrictions on Transitive Roles
IFIP Advances in Information and Communication Technology | 2010-10-27 | Paper |
Clausal graph tableaux for hybrid logic with eventualities and difference
Logic for Programming, Artificial Intelligence, and Reasoning | 2010-10-12 | Paper |
Terminating Tableaux for Hybrid Logic with Eventualities
Automated Reasoning | 2010-09-14 | Paper |
Analytic Tableaux for Simple Type Theory and its First-Order Fragment
Logical Methods in Computer Science | 2010-07-27 | Paper |
Terminating tableau systems for hybrid logic with difference and converse
Journal of Logic, Language and Information | 2010-01-06 | Paper |
Terminating tableaux for the basic fragment of simple type theory
Lecture Notes in Computer Science | 2009-12-01 | Paper |
Terminating tableaux for graded hybrid logic with global modalities and role hierarchies
Lecture Notes in Computer Science | 2009-12-01 | Paper |
Extended First-Order Logic
Lecture Notes in Computer Science | 2009-10-20 | Paper |
Terminating Tableaux for Hybrid Logic with the Difference Modality and Converse
Automated Reasoning | 2008-11-27 | Paper |
Generating Propagators for Finite Set Constraints
Principles and Practice of Constraint Programming - CP 2006 | 2008-09-09 | Paper |
A concurrent lambda calculus with futures
Theoretical Computer Science | 2007-01-09 | Paper |
Frontiers of Combining Systems
Lecture Notes in Computer Science | 2006-10-10 | Paper |
scientific article; zbMATH DE number 1254033 (Why is no real title available?)
| 1999-10-25 | Paper |
Situated simplification
Theoretical Computer Science | 1998-07-23 | Paper |
scientific article; zbMATH DE number 1088220 (Why is no real title available?)
| 1997-11-17 | Paper |
scientific article; zbMATH DE number 1088219 (Why is no real title available?)
| 1997-11-17 | Paper |
scientific article; zbMATH DE number 970739 (Why is no real title available?)
| 1997-05-25 | Paper |
A complete and recursive feature theory
Theoretical Computer Science | 1997-02-28 | Paper |
A feature constraint system for logic programming with entailment
Theoretical Computer Science | 1994-11-29 | Paper |
Records for logic programming
The Journal of Logic Programming | 1994-05-05 | Paper |
On the expressivity of feature logics with negation, functional uncertainty, and sort equations
Journal of Logic, Language and Information | 1994-03-10 | Paper |
scientific article; zbMATH DE number 44623 (Why is no real title available?)
| 1993-01-23 | Paper |
scientific article; zbMATH DE number 67967 (Why is no real title available?)
| 1992-09-27 | Paper |
Feature-constraint logics for unification grammars
The Journal of Logic Programming | 1992-08-13 | Paper |
Attributive concept descriptions with complements
Artificial Intelligence | 1991-01-01 | Paper |
scientific article; zbMATH DE number 4164128 (Why is no real title available?)
| 1989-01-01 | Paper |
Inheritance hierarchies: Semantics and unifications
Journal of Symbolic Computation | 1989-01-01 | Paper |
Basic narrowing revisited
Journal of Symbolic Computation | 1989-01-01 | Paper |
Order-sorted unification
Journal of Symbolic Computation | 1989-01-01 | Paper |
scientific article; zbMATH DE number 3788022 (Why is no real title available?)
| 1982-01-01 | Paper |
