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