Papers by Christoph Kreitz in chronological order
Most of my publications are available online in postscript or pdf format.
An abstract with a complete reference and corresponding bibtex entry is also provided.
Abstract Mathematisches Argumentieren und Beweisen mit dem Theorembeweiser Coq
HDI2016 - 7. Fachtagung zur Hochschuldidaktik der Informatik, 2016.
PS Version PDF Version
Abstract Deductive Reasoning Systems
International Encyclopedia of the Social & Behavioral Sciences, 2015.
PS Version PDF Version
Abstract Teaching Theoretical Computer Science using a Cognitive Apprenticeship Approach
SIGCSE'14 - 45th ACM technical symposium on Computer science education, 2014.
PS Version PDF Version
Abstract Theoretical Computer Science Education in light of Cognitive Apprenticeship
Technical Report, Universität Potsdam, 2012.
PS Version PDF Version
Abstract Konstruktivistisch- und kompetenzorientierte Lehre der Theoretischen Informatik
5. Fachtagung zur Hochschuldidaktik der Informatik, 2012.
PS Version PDF Version
Abstract Nuprl as Logical Framework for Automating Proofs in Category Theory
Logic and Program Semantics, 2012.
PS Version PDF Version
Abstract Introduction to Classic ML
Technical Report, Cornell University, 2011.
PS Version PDF Version
Abstract Specifying and Verifying Organizational Security Properties in First-Order Logic
Verification, Induction, Termination Analysis, 2010.
PS Version PDF Version
Abstract LambdaMu-PRL - A Proof Refinement Calculus for Classical Reasoning in Computational
Type Theory
    Technical Report, Universität Potsdam, 2009.
PS Version PDF Version
Abstract Connection Method
Scholarpedia, 2009.
PS Version PDF Version
Abstract The ILTP Problem Library for Intuitionistic Logic
Journal of Automated Reasoning, 2007.
PS Version PDF Version
Abstract Formale Methoden der künstlichen Intelligenz
Künstliche Intelligenz, 2006.
PS Version PDF Version
Abstract Automating Proofs in Category Theory
IJCAR-2006, 2006.
PS Version PDF Version
Abstract Innovations in Computational Type Theory using Nuprl
Journal of Applied Logic, 2006.
PS Version PDF Version
Abstract The ILTP Library: Benchmarking Automated Theorem Provers for Intuitionistic Logic
TABLEAUX-2005, 2005.
PS Version PDF Version
Abstract A Matrix Characterization for Multiplicative Exponential Linear Logic
Journal of Automated Reasoning, 2004.
PS Version PDF Version
Abstract Building Reliable, High-Performance Networks with the Nuprl Proof Development System
Journal of Functional Programming, 2004.
PS Version PDF Version
Abstract Formal Derivation of an Algorithm for the Stamps Problem
Technical Memo, Cornell University, 2003.
PS Version PDF Version
Abstract Derivation of a Fast Integer Square Root Algorithm
Technical Memo, Cornell University, 2003.
PS Version PDF Version
Abstract Steps Toward a World Wide Digital Library of Formal Algorithmic Knowledge
Technical Report, Cornell University, 2003.
PS Version PDF Version
Abstract MetaPRL - A Modular Logical Environment
TPHOLs'03, 2003.
PS Version PDF Version
Abstract A Nuprl-PVS Connection: Integrating Libraries of Formal Mathematics
Technical Report, Cornell University, 2003.
PS Version PDF Version
Abstract The Nuprl Proof Development System, Version 5: Reference Manual and User's Guide
Technical Report, Cornell University, 2002.
PS Version PDF Version
Abstract User-specified Adaptive Scheduling in a Streaming Media Network.
Technical Report, Cornell University, 2002.
PS Version PDF Version
Abstract FDL: A Prototype Formal Digital Library
Technical Report, Cornell University, 2002.
PS Version PDF Version
Abstract Proving Hybrid Protocols Correct
TPHOLs 2001, 2001.
PS Version PDF Version
Abstract JProver: Integrating Connection-based Theorem Proving into Interactive Proof Assistants
IJCAR 2001, 2001.
PS Version PDF Version
Abstract Formally Verifying Hybrid Protocols with the Nuprl Logical Programming Environment
Technical Report, Cornell University, 2001.
PS Version PDF Version
Abstract An Experiment in Formal Design using Meta-Properties
DISCEX II, 2001.
PS Version PDF Version
Abstract Protocol Switching: Exploiting Meta-Properties
WARGC 2001, 2001.
PS Version PDF Version
Abstract Connection-Driven Inductive Theorem Proving
Studia Logica, 2001.
PS Version PDF Version
Abstract Matrix-based Inductive Theorem Proving.
TABLEAUX-2000, 2000.
PS Version PDF Version
Abstract The Nuprl Open Logical Environment
CADE-17, 2000.
PS Version PDF Version
Abstract A Uniform Procedure for Converting Matrix Proofs into Sequent-Style Systems
Information and Computation, 2000.
PS Version PDF Version
Abstract Matrix-based Constructive Theorem Proving.
Intellectics and Computation, 2000.
PS Version PDF Version
Abstract The Horus and Ensemble Projects: Accomplishments and Limitations.
DISCEX'00, 2000.
PS Version PDF Version
Abstract Building Reliable, High-Performance Systems from Components.
SOSP'99, 1999.
PS Version PDF Version
Abstract Automating Inductive Specification Proofs.
Fundamenta Informatica, 1999.
PS Version PDF Version
Abstract Connection-based Theorem Proving in Classical and Non-classical Logics.
Journal of Universal Computer Science, 1999.
PS Version PDF Version
Abstract Dependence Analysis Through Type Inference.
WoLLIC'99, 1999.
PS Version PDF Version
Abstract Automated Fast-Track Reconfiguration of Group Communication Systems.
TACAS 99, 1999.
PS Version PDF Version
Abstract Formal Reasoning about Communication Systems II: Automated Fast-Track
Reconfiguration.
    Technical Report, Cornell University, 1998.
PS Version PDF Version
Abstract Instantiation of Existentially Quantified Variables in Inductive Specification Proofs.
AISC'98, 1998.
PS Version PDF Version
Abstract A Matrix Characterization for MELL.
JELIA '98, 1998.
PS Version PDF Version
Abstract A Type-based Framework for Automatic Debugging
Technical Report, Cornell University, 1998.
PS Version PDF Version
Abstract Dead Code Elimination Through Type Inference
Technical Report, Cornell University, 1998.
PS Version PDF Version
Abstract A Proof Environment for the Development of Group Communication Systems.
CADE-15, 1998.
PS Version PDF Version
Abstract Program Synthesis.
In Automated Deduction - A Basis for Applications, Kluwer, 1998.
PS Version PDF Version
Abstract Deleting Redundancy in Proof Reconstruction.
TABLEAUX-98, 1998.
PS Version PDF Version
Abstract A multi-level approach to program synthesis.
LoPSTr'97, 1998.
PS Version PDF Version
Abstract Formal Reasoning about Communication Systems I: Embedding ML into Type Theory.
Technical Report, Cornell University, 1997.
PS Version PDF Version
Abstract Minimal and Complete Prefix Unification for Non-Classical Theorem Proving.
Technical Report, TU Darmstadt, 1997.
PS Version PDF Version
Abstract Connection-Based Proof Construction in Linear Logic
CADE-14, 1997.
PS Version PDF Version
Abstract Deciding Intuitionistic Propositional Logic via Translation into Classical Logic
CADE-14, 1997.
PS Version PDF Version
Abstract A Constructively Adequate Refutation System for Intuitionistic Logic
TABLEAUX-97, 1997.
PS Version PDF Version
Abstract Formal Reasoning about Modules, Reuse, Objects, and their Correctness.
FAPR'96, 1996.
PS Version PDF Version
Abstract Formal Mathematics for Verifiably Correct Program Synthesis.
Journal of the IGPL, 1996.
PS Version PDF Version
Abstract A Uniform Proof Procedure for Classical and Non-classical Logics.
KI-96, 1996.
PS Version PDF Version
Abstract Problem-Oriented Applications of Automated Theorem Proving.
DISCO '96, 1996.
PS Version PDF Version
Abstract Converting Non-Classical Matrix Proofs into Sequent-Style Systems.
CADE-13, 1996.
PS Version PDF Version
Abstract T-String-Unification: Unifying Prefixes in Non-Classical Proof Methods.
TABLEAUX-96, 1996.
PS Version PDF Version
Abstract Projektaufgaben in Anfängerveranstaltungen: ein Mittel zur Förderung eines
objektorientierten Programmierstils.
    GI Softwaretechnik-Trends, 1996.
PS Version PDF Version
Abstract Guiding Program Development Systems by a Connection Based Proof Strategy.
LoPSTr'95, 1996.
PS Version PDF Version
Abstract Logical Foundations for Declarative Object-oriented Programming
Technical Report, TU Darmstadt, 1995.
PS Version PDF Version
Abstract Integrating a Connection Based Proof Method into an Interactive Program Development
System.
    ProCos Workshop on Linking Theories, 1995.
PS Version PDF Version
Abstract Förderung des Guten - Änderung des Schlechten: 5 Thesen zur Verbesserung der
Grundlehre an der TH Darmstadt.
  TUD Werkstattgespräche zur Verbesserung der Lehre 1995.
PS Version PDF Version
Abstract Das Grundstudium an der TH Darmstadt aus studentischer Sicht - Analyse einer
fachübergreifenden Umfrage.
  TUD Werkstattgespräche zur Verbesserung der Lehre, 1995.
PS Version PDF Version
Abstract Lernen im Grundstudium: Orientierung - Beratung - Tutorien - Prüfungen.
TUD Werkstattgespräche zur Verbesserung der Lehre, 1995.
PS Version PDF Version
Abstract Lehr- und Lernformen in Studiengängen.
TU Darmstadt, Hochschuldidaktische Arbeitsstelle, 1995.
PS Version PDF Version
Abstract On Transforming Intuitionistic Matrix Proofs into Standard-Sequent Proofs.
TABLEAUX-95, 1995.
PS Version PDF Version
Abstract A Connection Based Proof Method for Intuitionistic Logic.
TABLEAUX-95, 1995.
PS Version PDF Version
Abstract On Testing Irreflexivity of Reduction Orderings for Combined Substitutions in
Intuitionistic Matrix Proofs.
    TABLEAUX-95, Short Papers, 1995.
PS Version PDF Version
Abstract A Foundation for Verified Software Development Systems.
Technical Report, TU Darmstadt, 1994.
PS Version PDF Version
Abstract Metasynthesis - Deriving Programs that Develop Programs.
Thesis for Habilitation, TU Darmstadt, 1992.
PS Version PDF Version
Abstract Deriving Strategies for the Design of Global Search Algorithms.
Technical Report, TU Darmstadt, 1992.
PS Version PDF Version
Abstract Konzeption eines Nebenfachstudiums "Sozialorientierte Gestaltung von
Informationstechnik".    
TU Darmstadt, 1992.
Not available online
Abstract Building proofs by Analogy via the Curry-Howard Isomorphism.
LPAR '92, 1992.
PS Version PDF Version
Abstract Type 2 computational complexity of functions on Cantor's space.
Theoretical Computer Science, 1991.
PS Version PDF Version
Abstract Towards a formal theory of program construction.
Revue d' Intelligence Artificielle, 1990.
PS Version PDF Version
Abstract The representation of program synthesis in higher order logic.
GWAI-90, 1990.
PS Version PDF Version
Abstract XPRTS - an implementation tool for program synthesis.
GWAI-89, 1989.
PS Version PDF Version
Abstract Logic Oriented Program Synthesis - goals and realization.
Technical Report, TU München, 1988.
PS Version PDF Version
Abstract Towards a flexible LOPS implementation: an example of XPRTS programming.
Technical Report, TU München, 1987.
PS Version PDF Version
Abstract Compactness in constructive analysis revisited.
Annals of pure and applied logic, 1987.
PS Version PDF Version
Abstract Representations of the real numbers and the open subsets of the set of real numbers.
Annals of pure and applied logic, 1987.
PS Version PDF Version
Abstract Constructive automata theory implemented with the NuPRL proof development system.
Technical Report, Cornell University, 1986
PS Version PDF Version
Abstract Theory of representations.
Theoretical Computer Science, 1985.
PS Version PDF Version
Abstract Theorie der Darstellungen und ihre Anwendungen in der konstruktiven Analysis.
PhD Thesis, Fernuniversität Hagen (German), 1984.
PS Version PDF Version
Abstract Towards a theory of representations.
2nd Frege Conference, 1984.
PS Version PDF Version
Abstract A unified approach to constructive and recursive analysis.
Logic Colloquium Aachen, 1984.
PS Version PDF Version
Abstract Complexity theory on real numbers and functions.
6th GI Conference on Theoretical Computer Science, 1983.
PS Version PDF Version
Abstract Zulässige CPO's - ein Entwurf für ein allgemeines Berechenbarkeitskonzept.
Diplomarbeit, RWTH Aachen, 1981.
PS Version PDF Version

BACK
Back to main page