| 2023 | CPP | A Computational Cantor-Bernstein and Myhill's Isomorphism Theorem in Constructive Type Theory (Proof Pearl). | Yannick Forster, Felix Jahn, Gert Smolka |
| 2021 | ITP | A Mechanised Proof of the Time Invariance Thesis for the Weak Call-By-Value λ-Calculus. | Yannick Forster, Fabian Kunze, Gert Smolka, Maxi Wuttke |
| 2019 | CPP | On synthetic undecidability in coq, with an application to the entscheidungsproblem. | Yannick Forster, Dominik Kirst, Gert Smolka |
| 2018 | APLAS | Formal Small-Step Verification of a Call-by-Value Lambda Calculus Machine. | Fabian Kunze, Gert Smolka, Yannick Forster |
| 2018 | CPP | Large model constructions for second-order ZF in dependent type theory. | Dominik Kirst, Gert Smolka |
| 2018 | ITP | Verification of PCP-Related Computational Reductions in Coq. | Yannick Forster, Edith Heiter, Gert Smolka |
| 2017 | CPP | Equivalence of system f and ź2 in Coq based on context morphism lemmas. | Jonas Kaiser, Tobias Tebbi, Gert Smolka |
| 2017 | ITP | Weak Call-by-Value Lambda Calculus as a Model of Computation in Coq. | Yannick Forster, Gert Smolka |
| 2017 | ITP | Categoricity Results for Second-Order ZF in Dependent Type Theory. | Dominik Kirst, Gert Smolka |
| 2016 | CPP | Axiomatic semantics for compiler verification. | Steven Schfer, Sigurd Schneider, Gert Smolka |
| 2016 | ITP | Two-Way Automata in Coq. | Christian Doczkal, Gert Smolka |
| 2016 | ITP | Hereditarily Finite Sets in Constructive Type Theory. | Gert Smolka, Kathrin Stark |
| 2015 | CPP | Completeness and Decidability of de Bruijn Substitution Algebra in Coq. | Steven Schfer, Gert Smolka, Tobias Tebbi |
| 2015 | ITP | Autosubst: Reasoning with de Bruijn Terms and Parallel Substitutions. | Steven Schfer, Tobias Tebbi, Gert Smolka |
| 2015 | ITP | A Linear First-Order Functional Intermediate Language for Verified Compilers. | Sigurd Schneider, Gert Smolka, Sebastian Hack |
| 2015 | ITP | Transfinite Constructions in Classical Type Theory. | Gert Smolka, Steven Schfer, Christian Doczkal |
| 2014 | ITP | Completeness and Decidability Results for CTL in Coq. | Christian Doczkal, Gert Smolka |
| 2013 | CPP | A Constructive Theory of Regular Languages in Coq. | Christian Doczkal, Jan-Oliver Kaiser, Gert Smolka |
| 2012 | CPP | Constructive Completeness for Modal Logic with Transitive Closure. | Christian Doczkal, Gert Smolka |
| 2011 | CPP | Constructive Formalization of Hybrid Logic with Eventualities. | Christian Doczkal, Gert Smolka |
| 2011 | TABLEAUX | Correctness and Worst-Case Optimality of Pratt-Style Decision Procedures for Modal and Hybrid Logics. | Mark Kaminski, Thomas Schneider, Gert Smolka |
| 2010 | CADE | Terminating Tableaux for Hybrid Logic with Eventualities. | Mark Kaminski, Gert Smolka |
| 2010 | LPAR | Clausal Graph Tableaux for Hybrid Logic with Eventualities and Difference. | Mark Kaminski, Gert Smolka |
| 2009 | TABLEAUX | Terminating Tableaux for the Basic Fragment of Simple Type Theory. | Chad E. Brown, Gert Smolka |
| 2009 | TABLEAUX | Terminating Tableaux for Graded Hybrid Logic with Global Modalities and Role Hierarchies. | Mark Kaminski, Sigurd Schneider, Gert Smolka |
| 2008 | CADE | Terminating Tableaux for Hybrid Logic with the Difference Modality and Converse. | Mark Kaminski, Gert Smolka |
| 2006 | CP | Generating Propagators for Finite Set Constraints. | Guido Tack, Christian Schulte, Gert Smolka |
| 2006 | FlAIRS | Multi-Dimensional Dependency Grammar as Multigraph Description. | Ralph Debusmann, Gert Smolka |
| 2004 | COLING | A Relational Syntax-Semantics Interface Based on Dependency Grammar. | Ralph Debusmann, Denys Duchier, Alexander Koller, Marco Kuhlmann, Gert Smolka, Stefan Thater |
| 1998 | ESOP | Concurrent Constraint Programming Based on Functional Programming (Extended Abstract). | Gert Smolka |
| 1996 | JELIA | The Oz Programming Model. | Gert Smolka |
| 1995 | CP | Situated Simplification. | Andreas Podelski, Gert Smolka |
| 1995 | EuroPar | The Oz Programming Model (Extended Abstract). | Gert Smolka |
| 1995 | ICLP | Operational Semantics of Constraint Logic Programs with Coroutining. | Andreas Podelski, Gert Smolka |
| 1995 | ICLP | Situated Simplification. | Andreas Podelski, Gert Smolka |
| 1995 | ICLP | Oz: Concurrent Constraint Programming for Real. | Gert Smolka |
| 1993 | ACL | A Complete and Recursive Feature Theory. | Rolf Backofen, Gert Smolka |
| 1993 | ICLP | A Survey of Oz - A Higher-order Concurrent Constraint Language. | Gert Smolka |
| 1993 | IJCAI | Oz - A Programming Language for Multi-Agent Systems. | Martin Henz, Gert Smolka, Jrg Wrtz |
| 1993 | KI | Object-Oriented Concurrent Constraint Programming in Oz. | Gert Smolka, Martin Henz, Jrg Wrtz |
| 1992 | ICLP | Records for Logic Programming. | Gert Smolka, Ralf Treinen |
| 1990 | CADE | Tutorial on Reasoning and Representation with Concept Languages. | Jrgen Mller, Franz Baader, Bernhard Nebel, Werner Nutt, Gert Smolka |
| 1989 | KI | Fachseminar: Formale und kognitive Grundlagen von Wissensreprsentationen. | Daniel Hernndez, Bernhard Nebel, Gert Smolka, Ipke Wachsmuth |
| 1989 | KI | Feature-Logik. | Gert Smolka |
| 1982 | KI | Completeness of the Connection Graph Proof Procedure for Unit-Refutable Clause Sets. | Gert Smolka |
| 1981 | IJCAI | The Markgraf Karl Refutation Procedure. | Karl-Hans Blsius, Norbert Eisinger, Jrg H. Siekmann, Gert Smolka, Alexander Herold, Christoph Walther |
| 1981 | KI | Selection Heuristics, Deletion Strategies and N-Level Terminator Configurations for the Connection Graph Proof Procedure. | Jrg H. Siekmann, Gert Smolka |
| 1980 | GI | Das Karlsruher Beweissystem. | Norbert Eisinger, Jrg H. Siekmann, Gert Smolka, E. Unvericht, Christoph Walther |