"Relating models of impredicative type theories." (1991)
"Analysing proofs in analysis" (1996)
- in: Mück A., Streicher T. and Lock H.
"A tiny constraint functional logic language and its continuation semantics." (1994)
- in: Otto M.
"Generalized quantifiers for simple properties" (1994)
- in: Altenkirch T., Hofmann M. and Streicher T.
"Categorical reconstruction of a reduction free normalization proof." (1995) - in: Otto M.
"Ptime canonization for two variables with counting" (1995)
- in: Altenkirch T., Hofmann M. and Streicher T.
"Reduction-free normalisation for a polymorphic system" (1996) - in: Kohlenbach U.
"Arithmetizing proofs in analysis" (1998) - in: Otto M.
"The logic of explicitly representation-invariant circuits" (1997) - in: Reus B. and Streicher T.
"General synthetic domain theory---a logical approach (extended abstract)" (1997)
"Capturing bisimulation-invariant Ptime" (1997)
"On the boundedness problem for two-variable first-order logic" (1998)
- in: Hoogland E., Marx M. and Otto M.
"Beth definability for the guarded fragment" (1999) - in: Marz M., Rohr A. and Streicher T.
"Full abstraction and universality via realisability" (1999) - in: Neven F., Otto M., Tyszkiewicz J. and Van Den Bussche J.
"Adding FOR-loops to first-order logic" (1999) - in: Otto M.
"Eliminating recursion in the mu-calculus" (1999)
- in: Ambos-Spies K., Brandt U. and Ziegler M.
"Real Benefit of Promises and Advice" (2013) - in: Otto M.
"Generalized quantifiers for simple properties" (1994)
