|
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.
|
|
|
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.
|
|
|
|
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.
|
Not available online
|
|
|
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.
|
Not available online
|
|
|
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.
|
Not available online
|
|
|
Towards a theory of representations.
2nd Frege Conference, 1984.
|
Not available online
|
|
|
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.
|
Not available online
|
Back to main page
|
|
|