| 2017 | ICER | Theorem Provers as a Learning Tool in Theory of Computation. | Maria Knobelsdorf, Christiane Frede, Sebastian Bhne, Christoph Kreitz |
| 2014 | SIGCSE | Teaching theoretical computer science using a cognitive apprenticeship approach. | Maria Knobelsdorf, Christoph Kreitz, Sebastian Bhne |
| 2006 | CADE | Automating Proofs in Category Theory. | Dexter Kozen, Christoph Kreitz, Eva Richter |
| 2005 | TABLEAUX | The ILTP Library: Benchmarking Automated Theorem Provers for Intuitionistic Logic. | Thomas Raths, Jens Otten, Christoph Kreitz |
| 2001 | CADE | JProver : Integrating Connection-Based Theorem Proving into Interactive Proof Assistants. | Stephan Schmitt, Lori Lorigo, Christoph Kreitz, Aleksey Nogin |
| 2000 | CADE | The Nuprl Open Logical Environment. | Stuart F. Allen, Robert L. Constable, Richard Eaton, Christoph Kreitz, Lori Lorigo |
| 2000 | TABLEAUX | Matrix-Based Inductive Theorem Proving. | Christoph Kreitz, Brigitte Pientka |
| 1999 | SOSP | Building reliable, high-performance communication systems from components. | Xiaoming Liu, Christoph Kreitz, Robbert van Renesse, Jason Hickey, Mark Hayden, Kenneth P. Birman, Robert L. Constable |
| 1999 | TACAS | Automated Fast-Track Reconfiguration of Group Communication Systems. | Christoph Kreitz |
| 1998 | AISC | Instantiation of Existentially Quantified Variables in Inductive Specification Proofs. | Brigitte Pientka, Christoph Kreitz |
| 1998 | CADE | A Proof Environment for the Development of Group Communication Systems. | Christoph Kreitz, Mark Hayden, Jason Hickey |
| 1998 | JELIA | A Matrix Characterization for MELL. | Heiko Mantel, Christoph Kreitz |
| 1998 | TABLEAUX | Deleting Redundancy in Proof Reconstruction. | Stephan Schmitt, Christoph Kreitz |
| 1997 | CADE | Deciding Intuitionistic Propositional Logic via Translation into Classical Logic. | Daniel S. Korn, Christoph Kreitz |
| 1997 | CADE | Connection-Based Proof Construction in Linear Logic. | Christoph Kreitz, Heiko Mantel, Jens Otten, Stephan Schmitt |
| 1997 | LOPSTR | A Multi-level Approach to Program Synthesis. | Wolfgang Bibel, Daniel S. Korn, Christoph Kreitz, F. Kurucz, Jens Otten, Stephen Schmitt, G. Stolpmann |
| 1996 | CADE | Converting Non-Classical Matrix Proofs into Sequent-Style Systems. | Stephan Schmitt, Christoph Kreitz |
| 1996 | KI | A Uniform Proof Procedure for Classical and Non-Classical Logics. | Jens Otten, Christoph Kreitz |
| 1996 | TABLEAUX | T-String Unification: Unifying Prefixes in Non-classical Proof Methods. | Jens Otten, Christoph Kreitz |
| 1995 | LOPSTR | Guiding Program Development Systems by a Connection Based Proof Strategy. | Christoph Kreitz, Jens Otten, Stephan Schmitt |
| 1995 | TABLEAUX | On Transforming Intuitionistic Matrix Proofs into Standard-Sequent Proofs. | Stephan Schmitt, Christoph Kreitz |
| 1992 | LPAR | Building Proofs by Analogy via the Curry-Horward Isomorphism. | Thierry Boy de la Tour, Christoph Kreitz |
| 1990 | KI | The Representation of Program Synthesis in Higher Order Logic. | Christoph Kreitz |
| 1989 | KI | XPRTS - An Implementation Tool for Program Synthesis. | Gerd Neugebauer, Bertram Fronhfer, Christoph Kreitz |