| Publication | Date of Publication | Type |
|---|
| A certified algorithm for AC-unification | 2024-05-27 | Paper |
| Grammar Compression by Induced Suffix Sorting | 2024-04-14 | Paper |
| Nominal AC-matching | 2024-02-28 | Paper |
| Formal verification of termination criteria for first-order recursive functions | 2024-02-06 | Paper |
| https://portal.mardi4nfdi.de/entity/Q6099621 | 2023-06-20 | Paper |
| Hall's theorem for enumerable families of finite sets | 2023-06-02 | Paper |
| Formalization of the computational theory of a Turing complete functional language model | 2022-12-12 | Paper |
| A certified functional nominal C-unification algorithm | 2022-08-25 | Paper |
| Formalization of ring theory in PVS. Isomorphism theorems, principal, prime and maximal ideals, Chinese remainder theorem | 2022-01-21 | Paper |
| Formalising nominal C-unification generalised with protected variables | 2022-01-20 | Paper |
| Formalising confluence in PVS | 2021-12-02 | Paper |
| Nominal equational problems | 2021-10-18 | Paper |
| Fixed-point constraints for nominal equational unification | 2021-06-15 | Paper |
| Elementary deduction problem for locally stable theories with normal forms | 2021-06-08 | Paper |
| Formalizing the confluence of orthogonal rewriting systems | 2021-06-08 | Paper |
| On solving nominal disunification constraints | 2021-01-19 | Paper |
| On nominal syntax and permutation fixed points | 2020-02-17 | Paper |
| A formalisation of nominal C-matching through unification with protected variables | 2019-11-13 | Paper |
| Formalization in PVS of balancing properties necessary for proving security of the Dolev-Yao cascade protocol model | 2019-09-18 | Paper |
| A formalisation of nominal \(\alpha\)-equivalence with A, C, and AC function symbols | 2019-06-25 | Paper |
| Typed path polymorphism | 2019-06-25 | Paper |
| Explicit substitution calculi with de Bruijn indices and intersection type systems | 2019-01-08 | Paper |
| First-order unification in the PVS proof assistant | 2019-01-08 | Paper |
| Applied logic for computer scientists. Computational deduction and formal proofs | 2018-11-29 | Paper |
| Formalization of the undecidability of the halting problem for a functional language | 2018-10-18 | Paper |
| Nominal C-unification | 2018-09-06 | Paper |
| Nominal essential intersection types | 2018-06-18 | Paper |
| Checking overlaps of nominal rewriting rules | 2018-04-23 | Paper |
| Completeness in PVS of a nominal unification algorithm | 2018-04-23 | Paper |
| Type soundness for path polymorphism | 2018-04-23 | Paper |
| A formalisation of nominal \(\alpha\)-equivalence with A and AC function symbols | 2018-04-23 | Paper |
| Intruder deduction problem for locally stable theories with normal forms and inverses | 2018-02-09 | Paper |
| On solving nominal fixpoint equations | 2018-01-04 | Paper |
| On the average number of reversals needed to sort signed permutations | 2017-12-06 | Paper |
| Nominal narrowing | 2017-10-17 | Paper |
| Confluence of orthogonal term rewriting systems in the prototype verification system | 2017-07-06 | Paper |
| A practical semi-external memory method for approximate pattern matching | 2017-05-19 | Paper |
| https://portal.mardi4nfdi.de/entity/Q2978530 | 2017-04-25 | Paper |
| A PVS theory for term rewriting systems | 2015-03-18 | Paper |
| A flexible framework for visualisation of computational properties of general explicit substitutions calculi | 2015-03-18 | Paper |
| On the computability of relations on \(\lambda \)-terms and Rice's theorem -- the case of the expansion problem for explicit substitutions | 2014-03-31 | Paper |
| Applying ELAN strategies in simulating processors over simple architectures | 2013-08-23 | Paper |
| Comparing calculi of explicit substitutions with eta-reduction | 2013-04-19 | Paper |
| On automating the extraction of programs from proofs using product types | 2013-04-19 | Paper |
| Intersection type system with de Bruijn indices | 2011-03-30 | Paper |
| Reduction of the intruder deduction problem into equational elementary deduction for electronic purse protocols with blind signatures | 2010-09-29 | Paper |
| Intersection type systems and explicit substitutions calculi | 2010-09-29 | Paper |
| Verification of the Completeness of Unification Algorithms à la Robinson | 2010-09-29 | Paper |
| A variant of the Ford-Johnson algorithm that is more space efficient | 2010-01-29 | Paper |
| Explicit substitutions calculi with one step eta-reduction decided explicitly | 2009-12-18 | Paper |
| SUBSEXPL: a tool for simulating and comparing explicit substitutions calculi | 2009-11-30 | Paper |
| A formalization of Newman's and Yokouchi's lemmas in a higher-order language | 2009-07-27 | Paper |
| Principal Typings for Explicit Substitutions Calculi | 2008-06-19 | Paper |
| Higher-order unification: a structural relation between Huet's method and the one based on explicit substitutions | 2008-04-07 | Paper |
| Parallel strategies for the local biological sequence alignment in a cluster of workstations | 2007-02-14 | Paper |
| Experimental and Efficient Algorithms | 2005-11-30 | Paper |
| Logic for Programming, Artificial Intelligence, and Reasoning | 2005-11-10 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5693576 | 2005-09-26 | Paper |
| Comparing and implementing calculi of explicit substitutions with eta-reduction | 2005-06-01 | Paper |
| A linear time lower bound on McCreight and general updating algorithms for suffix trees | 2004-09-22 | Paper |
| A framework to visualize equivalences between computational models of regular languages. | 2003-01-21 | Paper |
| Unification via the \(\lambda s_e\)-style of explicit substitutions | 2002-06-19 | Paper |
| Church-Rosser property for conditional rewriting systems with built-in predicates as premises | 2002-04-03 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4237636 | 1999-04-13 | Paper |
