| 2023 | CADE | Towards Fast Nominal Anti-unification of Letrec-Expressions. | Manfred Schmidt-Schau, Daniele Nantes-Sobrinho |
| 2022 | FSCD | Nominal Anti-Unification with Atom-Variables. | Manfred Schmidt-Schau, Daniele Nantes-Sobrinho |
| 2022 | PPDP | Contextual Equivalence in a Probabilistic Call-by-Need Lambda-Calculus. | David Sabel, Manfred Schmidt-Schau, Luca Maio |
| 2020 | LOPSTR | Nominal Unification with Letrec and Environment-Variables. | Manfred Schmidt-Schau, Yunus D. K. Kutz |
| 2018 | PPDP | Sequential and Parallel Improvements in a Concurrent Functional Programming Language. | Manfred Schmidt-Schau, David Sabel, Nils Dallmeyer |
| 2016 | LOPSTR | Nominal Unification of Higher Order Expressions with Recursive Let. | Manfred Schmidt-Schau, Temur Kutsia, Jordi Levy, Mateu Villaret |
| 2016 | PPDP | Unification of program expressions with recursive bindings. | Manfred Schmidt-Schau, David Sabel |
| 2015 | CSL | Two-Restricted One Context Unification is in Polynomial Time. | Adri Gascn, Manfred Schmidt-Schau, Ashish Tiwari |
| 2015 | LICS | One Context Unification Problems Solvable in Polynomial Time. | Adri Gascn, Ashish Tiwari, Manfred Schmidt-Schau |
| 2015 | PPDP | Improvements in a functional core language with call-by-need operational semantics. | Manfred Schmidt-Schau, David Sabel |
| 2014 | CSR | Processing Succinct Matrices and Vectors. | Markus Lohrey, Manfred Schmidt-Schau |
| 2013 | ICFP | Correctness of an STM Haskell implementation. | Manfred Schmidt-Schau, David Sabel |
| 2012 | CADE | Correctness of Program Transformations as a Termination Problem. | Conrad Rau, David Sabel, Manfred Schmidt-Schau |
| 2012 | LICS | Conservative Concurrency in Haskell. | David Sabel, Manfred Schmidt-Schau |
| 2011 | PPDP | A contextual semantics for concurrent Haskell with futures. | David Sabel, Manfred Schmidt-Schau |
| 2009 | FOSSACS | Parameter Reduction in Grammar-Compressed Trees. | Markus Lohrey, Sebastian Maneth, Manfred Schmidt-Schau |
| 2009 | GI | Reasoning about Contextual Equivalence: From Untyped to Polymorphically Typed Calculi. | David Sabel, Manfred Schmidt-Schau, Frederik Harwath |
| 2008 | LICS | Context Matching for Compressed Terms. | Adri Gascn, Guillem Godoy, Manfred Schmidt-Schau |
| 2006 | CADE | Stratified Context Unification Is NP-Complete. | Jordi Levy, Manfred Schmidt-Schau, Mateu Villaret |
| 2003 | CADE | Decidability of Arity-Bounded Higher-Order Matching. | Manfred Schmidt-Schau |
| 2002 | CSL | Decidability of Bounded Higher-Order Unification. | Manfred Schmidt-Schau, Klaus U. Schulz |
| 2001 | CSL | Stratified Context Unification Is in PSPACE. | Manfred Schmidt-Schau |
| 2001 | ICCS | A Term-Based Approach to Project Scheduling. | Pok-Son Kim, Manfred Schmidt-Schau |
| 1999 | CADE | Solvability of Context Equations with Two Context Variables is Decidable. | Manfred Schmidt-Schau, Klaus U. Schulz |
| 1998 | ICFP | A Non-Deterministic Call-by-Need Lambda Calculus. | Arne Kutzner, Manfred Schmidt-Schau |
| 1997 | SAS | TEA: Automatically Proving Termination of Programs in a Non-strict Higher-Order Functional Language. | Sven Eric Panitz, Manfred Schmidt-Schau |
| 1995 | SAS | Abstract Reduction Using a Tableau Calculus | Manfred Schmidt-Schau, Sven Eric Panitz, Marko Schtz |
| 1993 | LPAR | Unification Under One-Sided Distributivity with a Multiplicative Unit. | Manfred Schmidt-Schau |
| 1990 | ECAI | Subsumption Algorithms for Concept Description Languages. | Bernhard Hollunder, Werner Nutt, Manfred Schmidt-Schau |
| 1989 | KR | Subsumption in KL-ONE is Undecidable. | Manfred Schmidt-Schau |
| 1988 | CADE | Unification in a Combination of Arbitrary Disjoint Equational Theories. | Manfred Schmidt-Schau |
| 1988 | LICS | Unification in Free Extensions of Boolean Rings and Abelian Groups | Alexandre Boudet, Jean-Pierre Jouannaud, Manfred Schmidt-Schau |
| 1986 | CADE | Unification in Many-Sorted Eqational Theories. | Manfred Schmidt-Schau |
| 1985 | IJCAI | A Many-Sorted Calculus with Polymorphic Functions Based on Resolution and Paramodulation. | Manfred Schmidt-Schau |
| 1985 | KI | Unification in a Many-sorted Calculus with Declarations. | Manfred Schmidt-Schau |