Theory of representations C Kreitz, K Weihrauch Theoretical computer science 38, 35-53, 1985 | 206 | 1985 |

Building reliable, high-performance communication systems from components X Liu, C Kreitz, R Van Renesse, J Hickey, M Hayden, K Birman, ... ACM SIGOPS Operating Systems Review 33 (5), 80-92, 1999 | 180 | 1999 |

The Horus and Ensemble projects: Accomplishments and limitations K Birman, B Constable, M Hayden, J Hickey, C Kreitz, R Van Renesse, ... Proceedings DARPA Information Survivability Conference and Exposition …, 2000 | 123 | 2000 |

Innovations in computational type theory using Nuprl SF Allen, M Bickford, RL Constable, R Eaton, C Kreitz, L Lorigo, E Moran Journal of Applied Logic 4 (4), 428-469, 2006 | 122 | 2006 |

Model elimination and connection tableau procedures C KREITZ | 107 | 2001 |

The *Nuprl* Open Logical EnvironmentSF Allen, RL Constable, R Eaton, C Kreitz, L Lorigo Automated Deduction-CADE-17: 17th International Conference on Automated …, 2000 | 90 | 2000 |

The ILTP problem library for intuitionistic logic: release v1. 1 T Raths, J Otten, C Kreitz Journal of Automated Reasoning 38, 261-271, 2007 | 81 | 2007 |

Representations of the real numbers and of the open subsets of the set of real numbers K Weihrauch, C Kreitz Annals of Pure and Applied Logic 35, 247-260, 1987 | 72 | 1987 |

Connection-based Theorem Proving in Classical and Non-classical Logics. C Kreitz, J Otten J. Univers. Comput. Sci. 5 (3), 88-112, 1999 | 69 | 1999 |

MetaPRL–a modular logical environment J Hickey, A Nogin, RL Constable, BE Aydemir, E Barzilay, Y Bryukhov, ... Theorem Proving in Higher Order Logics: 16th International Conference …, 2003 | 66 | 2003 |

JProver: Integrating connection-based theorem proving into interactive proof assistants S Schmitt, L Lorigo, C Kreitz, A Nogin Automated Reasoning: First International Joint Conference, IJCAR 2001 Siena …, 2001 | 61 | 2001 |

Protocol switching: Exploiting meta-properties X Liu, R van Renesse, M Bickford, C Kreitz, R Constable Proceedings 21st International Conference on Distributed Computing Systems …, 2001 | 60 | 2001 |

A connection based proof method for intuitionistic logic J Otten, C Kreitz International Workshop on Theorem Proving with Analytic Tableaux and Related …, 1995 | 60 | 1995 |

T-string unification: Unifying prefixes in non-classical proof methods J Otten, C Kreitz International Workshop on Theorem Proving with Analytic Tableaux and Related …, 1996 | 58 | 1996 |

A proof environment for the development of group communication systems C Kreitz, M Hayden, J Hickey Automated Deduction—CADE-15: 15th International Conference on Automated …, 1998 | 52 | 1998 |

On transforming intuitionistic matrix proofs into standard-sequent proofs S Schmitt, C Kreitz International Workshop on Theorem Proving with Analytic Tableaux and Related …, 1995 | 47 | 1995 |

A uniform proof procedure for classical and non-classical logics J Otten, C Kreitz Annual Conference on Artificial Intelligence, 307-319, 1996 | 45 | 1996 |

Teaching theoretical computer science using a cognitive apprenticeship approach M Knobelsdorf, C Kreitz, S Böhne Proceedings of the 45th ACM technical symposium on Computer science …, 2014 | 44 | 2014 |

The Nuprl Proof Development System, Version 5: Reference Manual and User’s Guide C Kreitz Department of Computer Science, Cornell University, 10, 2002 | 40 | 2002 |

Program synthesis C Kreitz Automated Deduction—A Basis for Applications: Volume III Applications, 105-134, 1998 | 40 | 1998 |