Slides of Talks by Christoph Kreitz
Slides are available in as postscript file, compressed with gzip, and as compressed pdf or PowerPoint file.
	The Nuprl Proof Development System Calculemus Autumn School, Pisa, Italy, September/October 2002.
	Formal Logical Environments for Building Reliable, High-Performance Software Harvey Mudd College, Claremont, CA, March 2002.
	Designing Reliable, High-Performance Networks with the Nuprl Logical Programming Environment AAAI Spring Symposium on Logic-Based Program Synthesis, Stanford University, Stanford, CA, March 2002.
	Enhancing Proof Assistant Systems Cornell University, Ithaca, NY, February 2002
	Proof Automation in Constructive Type Theory Cornell University, Ithaca, NY, September 2001
	Proving Hybrid Protocols Correct 14th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2001), Edinburgh, Scotland, September 2001.                     (Presentation: Mark Bickford)
	Designing Reliable, High-Performance Networks with the Nuprl Proof Development System Dagstuhl Workshop "Dependent Type Theory meets Practical Programming", Schloss Dagstuhl, Germany, August 2001.
	Advances in Logical Programming Environments Information Assurance Institute, Air Force Research Laboratory Rome, Rome, NY, July 2001.
	JProver: Integrating Connection-based Theorem Proving into Interactive Proof Assistants International Joint Conference on Automated Reasoning (IJCAR 2001), Siena, Italy, June 2001.                     (Presentation: Lori Lorigo)
	Formal Design and Verification: Challenges and Prospects IJCAR 2001 Workshop on Verification, Siena, Italy, June 2001.
	Formal Design of Reliable Software Systems       (POSTER) DARPA Information Survivability Conference and Exposition (DISCEX II), Anaheim, CA, June 2001.
	An open Logical Programming Environment DARPA PCES PI Meeting, St. Louis, MO, May 2001.
	Protocol Switching: Exploiting Meta-Properties International Workshop on Applied Reliable Group Communication (WARGC 2001), Phoenix, AZ, April 2001.                     (Presentation: Robbert van Renesse)	Not available online
	Advances in Logical Programming Environments DARPA PCES PI Meeting, San Diego, CA, February 2001.
	Protocol Optimization in Ensemble/Spinglass       (POSTER) DARPA FTN PI Meeting, St. Petersburgh, FL, January 2001.
	Eine logische Programmierumgebung für modulare Kommunikationssysteme University of Potsdam, Potsdam, Germany, November 2000.
	Building Reliable, High-Performance Systems from Components. Technical University of Darmstadt, Darmstadt, Germany, July 2000.
	The Nuprl Open Logical Environment Scottish Theorem Proving Meeting, University of St. Andrews, Scotland, July 2000.
	Matrix-based Inductive Theorem Proving.                     (the talk includes a separate PowerPoint animation) International Conference TABLEAUX-2000, University of St. Andrews, Scotland, July 2000.
	Matrix-based Inductive Theorem Proving. Carnegie Mellon University, Pittsburgh, PA, May 2000.                     (Presentation: Brigitte Pientka)
	The Nuprl Open Logical Environment 17th Conference on Automated Deduction (CADE-17), Carnegie Mellon University, Pittsburgh, PA, June 2000.             (Presentation: Lori Lorigo)
	The Horus and Ensemble Projects: Accomplishments and Limitations. DARPA Information Survivability Conference and Exposition (DISCEX 2000), Hilton Head, SC, January 2000.         (Presentation: Ken Birman)
	Building Reliable, High-Performance Systems from Components. 17th ACM Symposium on Operating System Principles (SOSP'99), Kiawah Island Resort, Charleston, SC, December 1999.         (Presentation: Robbert van Renesse)
	Dependence Analysis Through Type Inference. 6th Workshop on Logic, Language, Information and Computation (WoLLIC'99) Rio de Janeiro, Brazil, May 1999.         (Presentation: Ozan Hafizogullari)	Not available online
	Automated Fast-Track Reconfiguration of Group Communication Systems. 5th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'99), Amsterdam, The Netherlands, March 1999.
	A Logical Programming Environment for Group Communication Systems Cornell University, Ithaca, NY, December 1998. Technical University of Dresden, Dresden, Germany, November 1998. Technical University of Darmstadt, Darmstadt, Germany, March 1998. Kestrel Institute, Palo Alto, CA, October 1997.
	Matrix-based Constructive Theorem Proving Symposium in Honor of Wolfgang Bibel, Technical University of Darmstadt, Germany, October 1998.
	Instantiation of Existentially Quantified Variables in Inductive Specification Proofs. 4th International Conference on Artificial Intelligence and Symbolic Computation (AISC'98), Plattsburgh, NY, September 1998.         (Presentation: Brigitte Pientka)	Not available online
	A Matrix Characterization for MELL. 6th European Workshop on Logics in Artificial Intelligence (JELIA'98), Schloss Dagstuhl, Germany, October 1998.         (Presentation: Heiko Mantel)
	A Proof Environment for the Development of Group Communication Systems. 15th International Conference on Automated Deduction (CADE-15), Lindau, Germany, July 1998.
	Intuitionistic Proof Transformations and their Application to Constructive Program Synthesis CADE-15 Workshop on Proof Search in Type-Theoretic Languages, Lindau, Germany, July 1998.
	Finding Substitutions for Meta-Variables in Specification Proofs CADE-15 Workshop on Automation of Proof by Mathematical Induction, Lindau, Germany, July 1998.
	Deleting Redundancy in Proof Reconstruction. International Conference TABLEAUX-98, Oisterwijk, The Netherlands, May 1998.         (Presentation: Stephan Schmitt)
	Connection-Based Proof Construction in Linear Logic 14th International Conference on Automated Deduction (CADE-14), Townsville, Australia, July 1997.         (Presentation: Heiko Mantel)
	Deciding Intuitionistic Propositional Logic via Translation into Classical Logic 14th International Conference on Automated Deduction (CADE-14), Townsville, Australia, July 1997.         (Presentation: Daniel Korn)
	A Constructively Adequate Refutation System for Intuitionistic Logic 6th International Workshop on Theorem Proving with Analytic Tableaux and Related Methods (TABLEAUX'97), Nancy, France, May 1997.         (Presentation: Daniel Korn)
	A multi-level approach to program synthesis. 7th International Workshop on Logic Program Synthesis and Transformation (LoPSTr'97), Leuven, Belgium, July 1997.         (Presentation: Wolfgang Bibel)
	Proof Strategies in Intuitionistic Logic Dagstuhl Workshop "Deduction", Schloss Dagstuhl, Germany, February 1997.         (Presentation: Jens Otten)
	Finding Substitutions for Meta-Variables in Specification Proofs Cornell University, Ithaca, NY, May 1997.         (Presentation: Brigitte Pientka)
	Verifizierte Systeme für wissensbasierte Softwareentwicklung University of Linz, Linz, Austria, May 1997 Martin-Luther Universität, Halle, Germany, October 1996 Universität der Bundeswehr, München, Germany, October 1996
	Formal Reasoning about Modules, Reuse, Objects, and their Correctness. International Conference on Formal and Applied Practical Reasoning (FAPR'96), Bonn, Germany, June 1996.         (Presentation: Kung-Kiu Lau)	Not available online
	A Uniform Proof Procedure for Classical and Non-classical Logics. 20th German Annual Conference on Artificial Intelligence (KI-96), Dresden, Germany, September 1996.
	Problem-Oriented Applications of Automated Theorem Proving. 4th International Symposium on Design and Implementation of Symbolic Computation Systems (DISCO'96), University of Karlsruhe, Germany, September 1996.         (Presentation: Wolfgang Bibel)
	Converting Non-Classical Matrix Proofs into Sequent-Style Systems. 13th International Conference on Automated Deduction (CADE-13), Rutgers University, New Brunswick, NJ, June 1996.         (Presentation: Stephan Schmitt)
	Guiding Program Development Systems by a Connection Based Proof Strategy. Cornell University, Ithaca, NY, June 1996
	T-String-Unification: Unifying Prefixes in Non-Classical Proof Methods. 5th International Workshop on Theorem Proving with Analytic Tableaux and Related Methods (TABLEAUX'96), Terrasini, Italy, May 1996.         (Presentation: Jens Otten)
	Guiding Program Development Systems by a Connection Based Proof Strategy. 5th International Workshop on Logic Program Synthesis and Transformation (LoPSTr'95), Utrecht, The Netherlands, September 1995. Max-Plack Institut für Informatik (MPI), Saarbrücken, Germany, June 1995.
	Integrating a Connection Based Proof Method into an Interactive Program Development System. ProCos Workshop on Linking Theories, Vedbaek, Denmark, August 1995.         (Presentation: Jens Otten)
	Ein Fundament für Verifizierte Softwareentwicklungssysteme University of Konstanz, Konstanz, Germany, January 1996. University of Dortmund, Dortmund, Germany, June 1995. University of Münster, Münster, Germany, November 1994. Annual Meeting of the GI Fachgruppe "Deduktionssysteme", Technical University of Darmstadt, Germany, October 1994. University of Bremen, Bremen, Germany, September 1994.
	Projektaufgaben im ersten Semester zur Förderung eines objektorientierten Programmierstils. Workshop Eiffel in Schule und Hochschule, Technical University of Darmstadt, Germany, May 1995.
	On Transforming Intuitionistic Matrix Proofs into Standard-Sequent Proofs. 4th International Workshop on Theorem Proving with Analytic Tableaux and Related Methods (TABLEAUX'95), St. Goar, Germany, May 1995.         (Presentation: Stephan Schmitt)
	A Connection Based Proof Method for Intuitionistic Logic. 4th International Workshop on Theorem Proving with Analytic Tableaux and Related Methods (TABLEAUX'95), St. Goar, Germany, May 1995.         (Presentation: Jens Otten)
	On Testing Irreflexivity of Reduction Orderings for Combined Substitutions in Intuitionistic Matrix Proofs. 4th International Workshop on Theorem Proving with Analytic Tableaux and Related Methods (TABLEAUX'95),           (POSTER) St. Goar, Germany, May 1995.         (Presentation: Daniel Korn)
	Typentheorie als Grundlage verifizierter und effizienter Systeme zur Synthese von Programmen Arbeitstreffen "Typentheorie", University of Ulm, Germany, April 1994.	Not available online
	Formal Mathematics as Key Component of Deductive Tools Dagstuhl Workshop "Logical Theory of Program Construction", Schloss Dagstuhl, Germany, March 1994.	Not available online
	Verifizierte Systeme für wissensbasierte Softwareentwicklung University of Hamburg, Hamburg, Germany, November 1993.
	Philosophie des Intuitionismus und sein Einfluss auf die Informatik Technical University of Darmstadt, Darmstadt, Germnany, May 1993.
	M E T A - S Y N T H E S E: Synthese von Programmen, die Programme generieren University of Kiel, Kiel, Germany, December 1992        (German Slides) University of Giessen, Giessen, Germany, July 1991     (English Slides: METASYNTHESIS: Deriving programs that develop correct programs )
	Building proofs by Analogy via the Curry-Howard Isomorphism. International Conference on Logic Programming and Automated Reasoning (LPAR'92), 1992.         (Presentation: Thierry Boy de la Tour) GWAI-92 Workshop "Kontrolle von Problemlöseverfahren", Bonn, Germany, September 1992.
	Deriving Programs that Develop Programs Dagstuhl Workshop "Logical Theory of Program Development", Schloss Dagstuhl, Germany, February 1991.
	Typentheorie AG Mathematik, TU Darmstadt Darmstadt, Germany, February 1991	Not available online
	Realisierung deduktiver Mechanismen in der Typentheorie Annual Meeting of the GI Fachgruppe "Deduktionssysteme", Johanniskreuz, Germany, September 1990.
	The representation of program synthesis in higher order logic. German Workshop on Artificial Intelligence (GWAI'90), St. Eringerfeld, Germany, September 1990. University of Kaiserslautern, Kaiserslautern, Germany, December 1990.
	Formale Untersuchung und Implementierung deduktiver Mechanismen in der Programmierung mit Hilfe der intuitionistischen Typen Theorie Gesellschaft für Mathematik und Datenverarbeitung (GMD)   Karlsruhe, Germany, June 1990.
	Towards a formal Theory of Program Construction Kestrel Institute, Palo Alto, CA, December 1990. Technical University of Darmstadt, Darmstadt, Germany, May 1990.
	Implementierung deduktiver Mechanismen in der Typentheorie German Research Center for Artificial Intelligence (DFKI) Saarbrücken, Saarbrücken, Germany, May 1990.
	Formalizing Program Synthesis Cornell University, Ithaca, NY, September 1989.	Not available online
	LOPS: LOgische ProgrammSynthese Workshop "Verifikation, Konstruktion und Synthese von Programmen", Kaiserslautern, Germany, April 1989.	Not available online
	Verifikation und automatisches Beweisen Technical University of Darmstadt Darmstadt, Germany, December 1988.	Not available online
	Das interaktive Beweissystem NuPRL RWTH Aachen, Aachen, Germany, June 1987 ECRC, Munich, Germany, May 1987 Annual Meeting of the GI Fachgruppe "Deduktionssysteme", Munich, Germany, March 1987 FernUniversität Hagen, Hagen, Germany, November 1986,	Not available online
	Implementing Automata Theory with the NuPRL System Universität Kaiserslautern, Kaiserslautern, Germany, December 1986 SEKI-Forum, Universität Karlsruhe, Karlsruhe, Germany, October 1986 SRI International, Menlo Park, CA, July 1986 University of Texas, Austin, TX, June 1986 Duke University, Durham, NC, May 1986 Cornell University, Ithaca, NY, April 1986	Not available online
	Towards a theory of representations. 2nd Frege Conference, Schwerin, Germany, September 1984	Not available online
	A unified approach to constructive and recursive analysis. European Summer Meeting of the Association for Symbolic Logic, RWTH Aachen, Aachen, Germany, July 1983	Not available online
	Complexity theory on real numbers and functions. 6th GI Conference on Theoretical Computer Science, Dortmund, Germany, January 1983	Not available online
Back to main page