//
Skip to main content
PRL Project

Knowledge Base of
Publication Publications, Seminar Seminars, & Math Book Math Library

PhD theses from the project are accessible at the NCSTRL web site.

Browse by author | title | year | subject

Filter for: Christoph Kreitz

39 results


Seminar Wider Deployment of Nuprl
by Richard Eaton, Mark Bickford, Robert L. Constable, Christoph Kreitz
September 28, 2012

Publication Nuprl as Logical Framework for Automating Proofs in Category | cite »
by Christoph Kreitz
April 26, 2012

Publication Introduction to Classic ML | cite »
by Christoph Kreitz, Vincent Rahli
2011

Publication Automating Proofs in Category Theory | cite »
by Dexter Kozen, Christoph Kreitz, Eva Richter
2006

Publication Innovations in Computational Type Theory using Nuprl | cite »
by Stuart F. Allen, Mark Bickford, Robert L. Constable, Richard Eaton, Christoph Kreitz, Lori Lorigo, Evan Moran
2006

Seminar Microsoft's Spec#
by Christoph Kreitz
April 17, 2006

Seminar Constructive Proofs and Program Extraction
by Christoph Kreitz
February 23, 2004

Publication A Nuprl-PVS Connection: Integrating Libraries of Formal Mathematics | cite »
by Jon Kleinberg, Mark Bickford, Robert L. Constable, Richard Eaton, Christoph Kreitz
2003

Publication The FDL Navigator: Browsing and Manipulating Formal Content | cite »
by Christoph Kreitz
2003

Seminar The Calculemus Autumn School
by Christoph Kreitz, Sabina Petride, Matthew Fluet
October 28, 2002

Publication FDL: A Prototype Formal Digital Library
by Stuart F. Allen, Mark Bickford, Robert L. Constable, Richard Eaton, Christoph Kreitz, Lori Lorigo
2002

Seminar Enhancing Proof Assistant Systems
by Christoph Kreitz
February 25, 2002

Seminar Embedded Ststems
by Christoph Kreitz, Robert L. Constable
November 05, 2001

Seminar Proof Automation in Constructive Type Theory
by Christoph Kreitz
September 17, 2001

Publication An Experiment in Formal Design Using Meta-Properties | cite »
by Mark Bickford, Christoph Kreitz, Robbert van Renesse, Robert L. Constable
2001

Publication Connection-Driven Inductive Theorem Proving | cite »
by Christoph Kreitz, Brigitte Pientka
2001

Publication Formally Verifying Hybrid Protocols with the Nuprl Logical Programming Environment | cite »
by Mark Bickford, Christoph Kreitz, Robbert van Renesse
2001

Publication JProver: Integrating Connection-Based Theorem Proving into Interactive Proof Assistants | cite »
by Stephan Schmitt, Lori Lorigo, Christoph Kreitz, Aleksey Nogin
2001

Publication Protocol Switching: Exploiting Meta-Properties | cite »
by Xiaoming Liu, Robbert van Renesse, Mark Bickford, Christoph Kreitz, Robert L. Constable
2001

Publication Proving Hybrid Protocols Correct | cite »
by Mark Bickford, Christoph Kreitz, Robbert van Renesse, Xiaoming Liu
2001

Publication A Uniform Procedure for Converting Matrix Proofs into Sequent-Style Systems | cite »
by Christoph Kreitz, Stephan Schmitt
2000

Publication Matrix-Based Constructive Theorem Proving | cite »
by Christoph Kreitz, Jens Otten, Stephan Schmitt, Brigitte Pientka
2000

Publication Matrix-Based Inductive Theorem Proving | cite »
by Christoph Kreitz, Brigitte Pientka
2000

Publication The Horus and Ensemble Projects: Accomplishments and Limitations | cite »
by Kenneth Birman, Robert L. Constable, Mark Hayden, Jason Hickey, Christoph Kreitz, Robbert van Renesse, Ohad Rodeh, Werner Vogels
2000

Publication The Nuprl Open Logical Environment | cite »
by Stuart F. Allen, Robert L. Constable, Richard Eaton, Christoph Kreitz, Lori Lorigo
2000

Publication Automated Fast-Track Reconfiguration of Group Communication Systems | cite »
by Christoph Kreitz
1999

Publication Automating Inductive Specification Proofs | cite »
by Brigitte Pientka, Christoph Kreitz
1999

Publication Building Reliable, High-Performance Communication Systems from Components | cite »
by Xiaoming Liu, Christoph Kreitz, Robbert van Renesse, Jason Hickey, Mark Hayden, Kenneth Birman, Robert L. Constable
1999

Publication Connection-Based Theorem Proving in Classical and Non-Classical Logics | cite »
by Christoph Kreitz, Jens Otten
1999

Publication Dependence Analysis Through Type Inference | cite »
by Ozan Hafizogullari, Christoph Kreitz
1999

Publication A Matrix Characterization for MELL | cite »
by Heiko Mantel, Christoph Kreitz
1998

Publication A Proof Environment for the Development of Group Communication Systems | cite »
by Christoph Kreitz, Mark Hayden, Jason Hickey
1998

Publication Formal Reasoning About Communication Systems II: Automated Fast-Track Reconfiguration | cite »
by Christoph Kreitz
1998

Publication Instantiation of Existentially Quantified Variables in Inductive Specification Proofs | cite »
by Brigitte Pientka, Christoph Kreitz
1998

Seminar Dead Code Elimination
by Ozan Hafizogullari, Christoph Kreitz
January 27, 1998

Publication Formal Reasoning About Communication Systems I: Embedding ML in Type Theory | cite »
by Christoph Kreitz
1997

Seminar Formal Reasoning about Communication Systems
by Christoph Kreitz
1996-1997

Publication Meta-Synthesis: Deriving Programs That Develop Programs | cite »
by Christoph Kreitz
1992

Publication Constructive Automata Theory Implemented with the Nuprl Proof Development System | cite »
by Christoph Kreitz
1986