| 2011 | CSL | Relative Completeness for Logics of Functional Programs. | Bernhard Reus, Thomas Streicher |
| 2006 | CSL | Universality Results for Models in Locally Boolean Domains. | Tobias Lw, Thomas Streicher |
| 2005 | ICALP | About Hoare Logics for Higher-Order Store. | Bernhard Reus, Thomas Streicher |
| 2002 | LICS | Semantics and Logic of Object Calculi. | Bernhard Reus, Thomas Streicher |
| 1999 | LICS | Full Abstraction and Universality via Realisability. | Michael Marz, Alexander Rohr, Thomas Streicher |
| 1997 | LICS | Induction and Recursion on the Partial Real Line via Biquotients of Bifree Algebras. | Martn Htzel Escard, Thomas Streicher |
| 1997 | LICS | Continuation Models are Universal for Lambda-Mu-Calculus. | Martin Hofmann, Thomas Streicher |
| 1996 | LICS | Reduction-Free Normalisation for a Polymorphic System. | Thorsten Altenkirch, Martin Hofmann, Thomas Streicher |
| 1994 | ESOP | A Tiny Constrain Functional Logic Language and Its Continuation Semantics. | Andy Mck, Thomas Streicher |
| 1994 | LICS | The Groupoid Model Refutes Uniqueness of Identity Proofs | Martin Hofmann, Thomas Streicher |
| 1993 | MFCS | Verifying Properties of Module Construction in Type Theory. | Bernhard Reus, Thomas Streicher |
| 1991 | LICS | Games Semantics for Linear Logic | Yves Lafont, Thomas Streicher |