On the consistency strength of 'Accessible' Jonsson Cardinals and of the Weak Chang Conjecture. - Hans-Dieter Donder; Peter Koepke (Ann. Pure Appl. Log., 1983)

The Consistency Strength of the Free-Subset Property for omegaomega. - Peter Koepke (J. Symb. Log., 1984)

Some applications of short core models. - Peter Koepke (Ann. Pure Appl. Log., 1988)

On the free subset property at singular cardinals. - Peter Koepke (Arch. Math. Log., 1989)

On the elimination of Malitz quantifiers over Archimedian real closed fields. - Peter Koepke (Arch. Math. Log., 1989)

Superatomic Boolean Algebras Constructed from Morasses. - Peter Koepke; Juan Carlos Martínez (J. Symb. Log., 1995)

An elementary approach to the fine structure of L. - Sy D. Friedman; Peter Koepke (Bull. Symb. Log., 1997)

Extenders, Embedding Normal Forms, and the Martin-Steel-Theorem. - Peter Koepke (J. Symb. Log., 1998)

A refinement of Jensen's constructible hierarchy. - Peter Koepke; Marc van Eijmeren (FotFS, 2001)

The Category of Inner Models. - Peter Koepke (Synth., 2002)

ProofML - eine Annotationssprache für natürliche Beweise. - Peter Koepke; Bernhard Schröder (LDV Forum, 2003)

Computing a Model of Set Theory. - Peter Koepke (CiE, 2005)

Turing computations on ordinals. - Peter Koepke (Bull. Symb. Log., 2005)

Infinite Time Register Machines. - Peter Koepke (CiE, 2006)

The Consistency Strength of Àw and Àw1 Being Rowbottom Cardinals Without the Axiom of Choice. - Arthur W. Apter; Peter Koepke (Arch. Math. Log., 2006)

Homogeneously Souslin sets in small inner models. - Peter Koepke; Ralf Schindler (Arch. Math. Log., 2006)

Hyperfine structure theory and gap 1 morasses. - Sy-David Friedman; Peter Koepke; Boris Piwinger (J. Symb. Log., 2006)

Ordinal computations. - Peter Koepke; Martin Koerwien (Math. Struct. Comput. Sci., 2006)

An Enhanced Theory of Infinite Time Register Machines. - Peter Koepke; Russell G. Miller (CiE, 2008)

Making all cardinals almost Ramsey. - Arthur W. Apter; Peter Koepke (Arch. Math. Log., 2008)

Register computations on ordinals. - Peter Koepke; Ryan Siders (Arch. Math. Log., 2008)

Minimality considerations for ordinal computers modeling constructibility. - Peter Koepke; Ryan Siders (Theor. Comput. Sci., 2008)

Ordinal Computability. - Peter Koepke (CiE, 2009)

The Naproche Project Controlled Natural Language Proof Checking of Mathematical Texts. - Marcos Cramer; Bernhard Fisseni; Peter Koepke; Daniel Kühlwein; Bernhard Schröder; Jip Veldman (CNL, 2009)

The Naproche Project: Controlled Natural Language Proof Checking of Mathematical Texts. - Marcos Cramer; Peter Koepke; Daniel Kühlwein; Bernhard Schröder; Jip Veldman (CNL (Pre-Proceedings), 2009)

Ordinal machines and admissible recursion theory. - Peter Koepke; Benjamin Seyfferth (Ann. Pure Appl. Log., 2009)

Premise Selection in the Naproche System. - Marcos Cramer; Peter Koepke; Daniel Kühlwein; Bernhard Schröder (IJCAR, 2010)

The basic theory of infinite time register machines. - Merlin Carl; Tim Fischbach; Peter Koepke; Russell G. Miller; Miriam Nasfi; Gregor Weckbecker (Arch. Math. Log., 2010)

The consistency strength of choiceless failures of SCH. - Arthur W. Apter; Peter Koepke (J. Symb. Log., 2010)

A Generalised Dynamical System, Infinite Time Register Machines, and $ Pi^1_1$ -CA0. - Peter Koepke; Philip D. Welch (CiE, 2011)

Parsing and Disambiguation of Symbolic Mathematics in the Naproche System. - Marcos Cramer; Peter Koepke; Bernhard Schröder (Calculemus/MKM, 2011)

Global square and mutual stationarity at the alephn. - Peter Koepke; Philip D. Welch (Ann. Pure Appl. Log., 2011)

Towards a Theory of Infinite Time Blum-Shub-Smale Machines. - Peter Koepke; Benjamin Seyfferth (CiE, 2012)

Transition of Consistency and Satisfiability under Language Extensions. - Julian J. Schlöder; Peter Koepke (Formaliz. Math., 2012)

The Gödel Completeness Theorem for Uncountable Languages. - Julian J. Schlöder; Peter Koepke (Formaliz. Math., 2012)

A minimal Prikry-type forcing for singularizing a measurable cardinal. - Peter Koepke; Karen Räsch; Philipp Schlicht (J. Symb. Log., 2013)

The first measurable cardinal can be the first uncountable regular cardinal at any successor height. - Arthur W. Apter; Ioanna M. Dimitriou; Peter Koepke (Math. Log. Q., 2014)

All uncountable cardinals in the Gitik model are almost Ramsey and carry Rowbottom filters. - Arthur W. Apter; Ioanna M. Dimitriou; Peter Koepke (Math. Log. Q., 2016)

Automatic Proof-Checking of Ordinary Mathematical Texts. - Steffen Frerix; Peter Koepke (CICM Workshops, 2018)

Textbook Mathematics in the Naproche-SAD System. - Peter Koepke (CICM Workshops, 2019)

Interpreting Mathematical Texts in Naproche-SAD. - Adrian De Lon; Peter Koepke; Anton Lorenzen (CICM, 2020)

The Isabelle/Naproche Natural Language Proof Assistant. - Adrian De Lon; Peter Koepke; Anton Lorenzen; Adrian Marti; Marcel Schütz; Makarius Wenzel (CADE, 2021)

A Natural Formalization of the Mutilated Checkerboard Problem in Naproche. - Adrian De Lon; Peter Koepke; Anton Lorenzen (ITP, 2021)

Preface. - Peter Koepke; Dennis Müller 001 (CICM Workshops, 2021)

Natural Typesetting of Naproche Formalizations in LaTeX (short paper). - Peter Koepke; Tim Lichtnau; Jonas Lippert (CICM Workshops, 2021)

Beautiful Formalizations in Isabelle/Naproche. - Adrian De Lon; Peter Koepke; Anton Lorenzen; Adrian Marti; Marcel Schütz; Erik Sturzenhecker (CICM, 2021)

CICM'22 System Entries. - Peter Koepke; Anton Lorenzen; Boris Shminke (CICM, 2022)