| Publication | Date of Publication | Type |
|---|
| Program equivalence in a typed probabilistic call-by-need functional language | 2023-09-25 | Paper |
| An algorithm for distributive unification | 2022-12-09 | Paper |
| Nominal Unification and Matching of Higher Order Expressions with Recursive Let | 2022-05-16 | Paper |
| Nominal unification with letrec and environment-variables | 2022-03-23 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5020947 | 2022-01-07 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4993360 | 2021-06-15 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3388524 | 2021-05-05 | Paper |
| Rewriting with generalized nominal unification | 2020-12-08 | Paper |
| A note on unification, subsumption and unification type | 2020-06-04 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5111911 | 2020-05-27 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5240138 | 2019-10-24 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5240185 | 2019-10-24 | Paper |
| A non-deterministic call-by-need lambda calculus | 2019-09-26 | Paper |
| Linear pattern matching of compressed terms and polynomial rewriting | 2018-09-05 | Paper |
| Nominal unification with atom-variables | 2018-06-14 | Paper |
| Processing succinct matrices and vectors | 2017-10-20 | Paper |
| Nominal unification of higher order expressions with recursive let | 2017-10-13 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5351971 | 2017-08-31 | Paper |
| A non-deterministic call-by-need lambda calculus | 2017-08-21 | Paper |
| Conservative Concurrency in Haskell | 2017-05-16 | Paper |
| https://portal.mardi4nfdi.de/entity/Q2958387 | 2017-02-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q2958388 | 2017-02-01 | Paper |
| Unification and matching on compressed terms | 2015-09-17 | Paper |
| Observational Semantics for a Concurrent Lambda Calculus with Reference Cells and Futures | 2015-07-10 | Paper |
| Observational program calculi and the correctness of translations | 2015-04-01 | Paper |
| Correctness of an STM Haskell implementation | 2015-03-30 | Paper |
| Simulation in the Call-by-Need Lambda-Calculus with Letrec, Case, Constructors, and Seq | 2015-03-17 | Paper |
| Concurrent Programming Languages and Methods for Semantic Analyses (Extended Abstract of Invited Talk) | 2014-07-24 | Paper |
| Applicative May- and Should-Simulation in the Call-by-Value Lambda Calculus with AMB | 2014-07-24 | Paper |
| Processing succinct matrices and vectors | 2014-06-24 | Paper |
| A two-valued logic for properties of strict functional programs allowing partial functions | 2013-07-05 | Paper |
| Counterexamples to applicative simulation and extensionality in non-deterministic call-by-need lambda-calculi with letrec | 2013-04-04 | Paper |
| Correctness of Program Transformations as a Termination Problem | 2012-09-05 | Paper |
| Parameter reduction and automata evaluation for grammar-compressed trees | 2012-08-17 | Paper |
| Fast equality test for straight-line compressed strings | 2012-07-20 | Paper |
| On the complexity of Bounded Second-Order Unification and Stratified Context Unification | 2012-06-08 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5389151 | 2012-04-25 | Paper |
| Congruence Closure of Compressed Terms in Polynomial Time | 2011-10-07 | Paper |
| Closures of may-, should- and must-convergences for contextual equivalence | 2010-09-07 | Paper |
| Automated Deduction – CADE-19 | 2010-04-20 | Paper |
| Similarity implies equivalence in a class of non-deterministic call-by-need lambda calculi | 2010-04-14 | Paper |
| On generic context lemmas for higher-order calculi with sharing | 2010-03-29 | Paper |
| Context unification with one context variable | 2009-12-03 | Paper |
| Unification with Singleton Tree Grammars | 2009-06-30 | Paper |
| The Complexity of Monadic Second-Order Unification | 2009-06-22 | Paper |
| Rewriting Techniques and Applications | 2009-04-30 | Paper |
| Parameter Reduction in Grammar-Compressed Trees | 2009-03-31 | Paper |
| Stratified Context Unification Is NP-Complete | 2009-03-12 | Paper |
| Bounded Second-Order Unification Is NP-Complete | 2008-09-25 | Paper |
| A Finite Simulation Method in a Non-deterministic Call-by-Need Lambda-Calculus with Letrec, Constructors, and Case | 2008-08-28 | Paper |
| A call-by-need lambda calculus with locally bottom-avoiding choice: context lemma and correctness of transformations | 2008-08-15 | Paper |
| Safety of Nöcker's strictness analysis | 2008-08-15 | Paper |
| Deciding inclusion of set constants over infinite non-strict data structures | 2008-02-15 | Paper |
| Correctness of Copy in Calculi with Letrec | 2008-01-02 | Paper |
| Decidability of bounded higher-order unification | 2007-10-19 | Paper |
| Mechanizing Mathematical Reasoning | 2006-01-10 | Paper |
| The complexity of linear and stratified context matching problems | 2005-02-24 | Paper |
| Decidability of bounded second order unification | 2004-11-23 | Paper |
| A Decision Algorithm for Stratified Context Unification | 2003-09-16 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4411845 | 2003-07-10 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4783328 | 2002-12-04 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3149792 | 2002-09-26 | Paper |
| Solvability of context equations with two context variables is decidable | 2002-06-11 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4263157 | 1999-09-22 | Paper |
| Decidability of behavioural equivalence in unary PCF | 1999-04-28 | Paper |
| A decision algorithm for distributive unification | 1999-01-12 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3838760 | 1998-10-08 | Paper |
| Decidability of unification in the theory of one-sided distributivity and a multiplicative unit | 1997-03-06 | Paper |
| Modular termination of \(r\)-consistent and left-linear term rewriting systems | 1997-02-28 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4282529 | 1994-08-25 | Paper |
| Computational aspects of an order-sorted logic with term declarations | 1993-06-05 | Paper |
| Attributive concept descriptions with complements | 1991-01-01 | Paper |
| Unification in Boolean rings and Abelian groups | 1989-01-01 | Paper |
| Unification in a combination of arbitrary disjoint equational theories | 1989-01-01 | Paper |
| On equational theories, unification, and (un)decidability | 1989-01-01 | Paper |
| Unification in permutative equational theories is undecidable | 1989-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3493318 | 1989-01-01 | Paper |
| Implication of clauses is undecidable | 1988-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3811748 | 1988-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3779785 | 1987-01-01 | Paper |
| Unification under associativity and idempotence is of type nullary | 1986-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3786020 | 1986-01-01 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4723321 | 1986-01-01 | Paper |
| Problem corner: The Lion and the Unicorn | 1985-01-01 | Paper |
