Das Karlsruher Beweissystem. - Norbert Eisinger; Jörg H. Siekmann; Gert Smolka; E. Unvericht; Christoph Walther (GI Jahrestagung, 1980)

The Markgraf Karl Refutation Procedure. - Karl-Hans Bläsius; Norbert Eisinger; Jörg H. Siekmann; Gert Smolka; Alexander Herold; Christoph Walther (IJCAI, 1981)

Elimination of Redundant Links in Extended Connection Graphs. - Christoph Walther (GWAI, 1981)

A many-sorted calculus based on resolution and paramodulation. - Christoph Walther (1982)

A Many-Sorted Calculus Based on Resolution and Paramodulation. - Christoph Walther (IJCAI, 1983)

Unification in Many-Sorted Theories. - Christoph Walther (ECAI, 1984)

A Mechanical Solution of Schubert's Steamroller by Many-Sorted Resolution. - Christoph Walther (Artif. Intell., 1985)

The Karlsruhe Induction Theorem Proving System. - Susanne Biundo; Birgit Hummel; Dieter Hutter; Christoph Walther (CADE, 1986)

A Classification of Many-Sorted Unification Problems. - Christoph Walther (CADE, 1986)

Automatisches Beweisen. - Christoph Walther (KIFS, 1986)

A Many-Sorted Calculus Based on Resolution and Paramodulation. - Christoph Walther (Pitman / Morgan Kaufmann, 1987)

Many-Sorted Resolution. - Christoph Walther (KIFS, 1987)

Argument-Bounded Algorithms as a Basis for Automated Termination Proofs. - Christoph Walther (CADE, 1988)

Many-sorted unification. - Christoph Walther (J. ACM, 1988)

Many-Sorted Inferences in Automated Theorem Proving. - Christoph Walther (Sorts and Types in Artificial Intelligence, 1989)

Automatisierung von Terminierungsbeweisen. - Christoph Walther (Vieweg, 1991)

Computing Induction Axioms. - Christoph Walther (LPAR, 1992)

Combining Induction Axioms by Machine. - Christoph Walther (IJCAI, 1993)

Mathematical induction. - Christoph Walther (Handbook of Logic in Artificial Intelligence and Logic Programming (2), 1994)

Reusing Proofs. - Thomas Kolbe; Christoph Walther (ECAI, 1994)

On Proving the Termination of Algorithms by Machine. - Christoph Walther (Artif. Intell., 1994)

Patching Proofs for Reuse (Extended Abstract). - Thomas Kolbe; Christoph Walther (ECML, 1995)

Second-Order Matching modulo Evaluation: A Technique for Reusing Proofs. - Thomas Kolbe; Christoph Walther (IJCAI, 1995)

Termination of Theorem Proving by Reuse. - Thomas Kolbe; Christoph Walther (CADE, 1996)

Criteria for Termination. - Christoph Walther (Intellectics and Computational Logic, 2000)

Proving theorems by reuse. - Christoph Walther; Thomas Kolbe (Artif. Intell., 2000)

On Terminating Lemma Speculations. - Christoph Walther; Thomas Kolbe (Inf. Comput., 2000)

Semantik und Programmverifikation - Christoph Walther (Teubner, 2001)

Automatisches Beweisen. - Christoph Walther (Handbuch der Künstlichen Intelligenz, 2003)

About VeriFun. - Christoph Walther; Stephan Schweitzer (CADE, 2003)

A Machine-Verified Code Generator. - Christoph Walther; Stephan Schweitzer (LPAR, 2003)

Automated Termination Analysis for Incompletely Defined Programs. - Christoph Walther; Stephan Schweitzer (LPAR, 2004)

Verification in the Classroom. - Christoph Walther; Stephan Schweitzer (J. Autom. Reason., 2004)

Reasoning About Incompletely Defined Programs. - Christoph Walther; Stephan Schweitzer (LPAR, 2005)

Context Dependent Procedures and Computed Types in -eriFun. - Andreas Schlosser; Christoph Walther; Michael Gonder; Markus Aderhold (PLPV@IJCAR, 2006)

Fermat, Euler, Wilson - Three Case Studies in Number Theory. - Christoph Walther; Nathan Wasser (J. Autom. Reason., 2017)

Formally Verified Montgomery Multiplication. - Christoph Walther (CAV (2), 2018)

Verified Newton-Raphson Iteration for Multiplicative Inverses Modulo Powers of Any Base. - Christoph Walther (ACM Trans. Math. Softw., 2019)

A Largely Automated Verification of GHC's Natural Mergesort. - Christoph Walther (Go Where the Bugs Are, 2025)

Reasoning About Incompletely Defined Programs. - Christoph Walther (J. Autom. Reason., 2025)