Knowledge Base of
Publications, Seminars, & Math Library

Filter for: Christoph Kreitz

39 results

---

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

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

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

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

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

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

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

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

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

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

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

Enhancing Proof Assistant Systems
by Christoph Kreitz
February 25, 2002

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Formal Reasoning about Communication Systems
by Christoph Kreitz
1996-1997

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

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