Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
97 | Amy P. Felty, Douglas J. Howe, Frank A. Stomp |
Protocol Verification in Nuprl. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CAV ![In: Computer Aided Verification, 10th International Conference, CAV '98, Vancouver, BC, Canada, June 28 - July 2, 1998, Proceedings, pp. 428-439, 1998, Springer, 3-540-64608-6. The full citation details ...](Pics/full.jpeg) |
1998 |
DBLP DOI BibTeX RDF |
|
97 | Douglas J. Howe |
A Type Annotation Scheme for Nuprl. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 11th International Conference, TPHOLs'98, Canberra, Australia, September 27 - October 1, 1998, Proceedings, pp. 207-224, 1998, Springer, 3-540-64987-5. The full citation details ...](Pics/full.jpeg) |
1998 |
DBLP DOI BibTeX RDF |
|
97 | Douglas J. Howe |
Computational Metatheory in Nuprl. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CADE ![In: 9th International Conference on Automated Deduction, Argonne, Illinois, USA, May 23-26, 1988, Proceedings, pp. 238-257, 1988, Springer, 3-540-19343-X. The full citation details ...](Pics/full.jpeg) |
1988 |
DBLP DOI BibTeX RDF |
formal metamathematics, reflection, Theorem proving, type theory, constructive mathematics, tactics |
83 | James L. Caldwell |
Moving Proofs-As-Programs into Practice. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ASE ![In: 1997 International Conference on Automated Software Engineering, ASE 1997, Lake Tahoe, CA, USA, November 2-5, 1997, pp. 10-17, 1997, IEEE Computer Society, 0-8186-7961-1. The full citation details ...](Pics/full.jpeg) |
1997 |
DBLP DOI BibTeX RDF |
proofs-as-programs, constructive type theory, correct-by-construction programs, inductive proofs, Nuprl rewrite system, fixed-point combinators, untyped lambda calculus, specifications, partial evaluation, lambda calculus, hierarchical verifications |
79 | Pavel Naumov, Mark-Oliver Stehr, José Meseguer 0001 |
The HOL/NuPRL Proof Translator (A Practical Approach to Formal Interoperability). ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 14th International Conference, TPHOLs 2001, Edinburgh, Scotland, UK, September 3-6, 2001, Proceedings, pp. 329-345, 2001, Springer, 3-540-42525-X. The full citation details ...](Pics/full.jpeg) |
2001 |
DBLP DOI BibTeX RDF |
|
79 | Mark D. Aagaard, Miriam Leeser |
Verifying a Logic Synthesis Tool in Nuprl: A Case Study in Software Verification. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CAV ![In: Computer Aided Verification, Fourth International Workshop, CAV '92, Montreal, Canada, June 29 - July 1, 1992, Proceedings, pp. 69-81, 1992, Springer, 3-540-56496-9. The full citation details ...](Pics/full.jpeg) |
1992 |
DBLP DOI BibTeX RDF |
|
69 | Robert L. Constable |
ML Programming in Constructive Type Theory (abstract). ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 10th International Conference, TPHOLs'97, Murray Hill, NJ, USA, August 19-22, 1997, Proceedings, pp. 87, 1997, Springer, 3-540-63379-0. The full citation details ...](Pics/full.jpeg) |
1997 |
DBLP DOI BibTeX RDF |
|
62 | Carsten Schürmann, Mark-Oliver Stehr |
An Executable Formalization of the HOL/Nuprl Connection in the Metalogical Framework Twelf. ![Search on Bibsonomy](Pics/bibsonomy.png) |
LPAR ![In: Logic for Programming, Artificial Intelligence, and Reasoning, 13th International Conference, LPAR 2006, Phnom Penh, Cambodia, November 13-17, 2006, Proceedings, pp. 150-166, 2006, Springer, 3-540-48281-4. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
|
62 | Stuart F. Allen, Robert L. Constable, Richard Eaton, Christoph Kreitz, Lori Lorigo |
The Nuprl Open Logical Environment. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CADE ![In: Automated Deduction - CADE-17, 17th International Conference on Automated Deduction, Pittsburgh, PA, USA, June 17-20, 2000, Proceedings, pp. 170-176, 2000, Springer, 3-540-67664-3. The full citation details ...](Pics/full.jpeg) |
2000 |
DBLP DOI BibTeX RDF |
|
62 | James L. Caldwell |
Classical Propositional Decidability via Nuprl Proof Extraction. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 11th International Conference, TPHOLs'98, Canberra, Australia, September 27 - October 1, 1998, Proceedings, pp. 105-122, 1998, Springer, 3-540-64987-5. The full citation details ...](Pics/full.jpeg) |
1998 |
DBLP DOI BibTeX RDF |
|
62 | David A. Basin, Peter Del Vecchio |
Verification Of Combinational Logic in Nuprl. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Hardware Specification, Verification and Synthesis ![In: Hardware Specification, Verification and Synthesis: Mathematical Aspects, Mathematical Science Institute Workshop, Cornall University, Ithaca, New York, USA, July 5-7, 1989, Proceedings, pp. 333-357, 1989, Springer, 3-540-97226-9. The full citation details ...](Pics/full.jpeg) |
1989 |
DBLP DOI BibTeX RDF |
|
52 | Mark Bickford, Robert L. Constable, Joseph Y. Halpern, Sabina Petride |
Knowledge-Based Synthesis of Distributed Systems Using Event Structures. ![Search on Bibsonomy](Pics/bibsonomy.png) |
LPAR ![In: Logic for Programming, Artificial Intelligence, and Reasoning, 11th International Conference, LPAR 2004, Montevideo, Uruguay, March 14-18, 2005, Proceedings, pp. 449-465, 2004, Springer, 3-540-25236-3. The full citation details ...](Pics/full.jpeg) |
2004 |
DBLP DOI BibTeX RDF |
|
52 | Mark D. Aagaard, Miriam Leeser |
Verifying a Logic-Synthesis Algorithm and Implementation: A Case Study in Software Verification. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IEEE Trans. Software Eng. ![In: IEEE Trans. Software Eng. 21(10), pp. 822-833, 1995. The full citation details ...](Pics/full.jpeg) |
1995 |
DBLP DOI BibTeX RDF |
weak division, theorem proving, logic synthesis, Software verification, hardware verification |
52 | Paul B. Jackson |
Exploring Abstract Algebra in Constructive Type Theory. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CADE ![In: Automated Deduction - CADE-12, 12th International Conference on Automated Deduction, Nancy, France, June 26 - July 1, 1994, Proceedings, pp. 590-604, 1994, Springer, 3-540-58156-1. The full citation details ...](Pics/full.jpeg) |
1994 |
DBLP DOI BibTeX RDF |
|
48 | Aleksey Nogin, Alexei Kopylov, Xin Yu, Jason Hickey |
A computational approach to reflective meta-reasoning about languages with bindings. ![Search on Bibsonomy](Pics/bibsonomy.png) |
MERLIN ![In: ACM SIGPLAN International Conference on Functional Programming, Workshop on Mechanized reasoning about languages with variable binding, MERLIN 2005, Tallinn, Estonia, September 30, 2005, pp. 2-12, 2005, ACM, 978-1-59593-072-9. The full citation details ...](Pics/full.jpeg) |
2005 |
DBLP DOI BibTeX RDF |
MetaPRL, Nuprl, languages with bindings, programming language, reflection, experimentation, type theory, higher-order abstract syntax |
45 | James L. Caldwell |
Extracting General Recursive Program Schemes in Nuprl's Type Theory. ![Search on Bibsonomy](Pics/bibsonomy.png) |
LOPSTR ![In: Logic Based Program Synthesis and Transformation, 11th International Workshop, LOPSTR 2001, Paphos, Cyprus, November 28-30, 2001, Selected Papers, pp. 233-244, 2001, Springer, 3-540-43915-3. The full citation details ...](Pics/full.jpeg) |
2001 |
DBLP DOI BibTeX RDF |
|
45 | Amy P. Felty, Douglas J. Howe |
Hybrid Interactive Theorem Proving Using Nuprl and HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CADE ![In: Automated Deduction - CADE-14, 14th International Conference on Automated Deduction, Townsville, North Queensland, Australia, July 13-17, 1997, Proceedings, pp. 351-365, 1997, Springer, 3-540-63104-6. The full citation details ...](Pics/full.jpeg) |
1997 |
DBLP DOI BibTeX RDF |
|
45 | David A. Basin |
Building Theories in Nuprl. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Logic at Botik ![In: Logic at Botik '89, Symposium on Logical Foundations of Computer Science, Pereslav-Zalessky, USSR, July 3-8, 1989, Proceedings, pp. 12-25, 1989, Springer, 3-540-51237-3. The full citation details ...](Pics/full.jpeg) |
1989 |
DBLP DOI BibTeX RDF |
|
45 | Douglas J. Howe |
Implementing Number Theory: An Experiment with Nuprl. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CADE ![In: 8th International Conference on Automated Deduction, Oxford, England, July 27 - August 1, 1986, Proceedings, pp. 404-415, 1986, Springer, 3-540-16780-3. The full citation details ...](Pics/full.jpeg) |
1986 |
DBLP DOI BibTeX RDF |
|
35 | Roderick Moten |
Exploiting Parallelism in Interactive Theorem Provers. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 11th International Conference, TPHOLs'98, Canberra, Australia, September 27 - October 1, 1998, Proceedings, pp. 315-330, 1998, Springer, 3-540-64987-5. The full citation details ...](Pics/full.jpeg) |
1998 |
DBLP DOI BibTeX RDF |
|
35 | Christoph Kreitz, Mark Hayden, Jason Hickey |
A Proof Environment for the Development of Group Communication Systems. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CADE ![In: Automated Deduction - CADE-15, 15th International Conference on Automated Deduction, Lindau, Germany, July 5-10, 1998, Proceedings, pp. 317-332, 1998, Springer, 3-540-64675-2. The full citation details ...](Pics/full.jpeg) |
1998 |
DBLP DOI BibTeX RDF |
|
35 | James A. Altucher, Prakash Panangaden |
A Mechanically Assisted Constructive Proof in Category Theory. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CADE ![In: 10th International Conference on Automated Deduction, Kaiserslautern, FRG, July 24-27, 1990, Proceedings, pp. 500-513, 1990, Springer, 3-540-52885-7. The full citation details ...](Pics/full.jpeg) |
1990 |
DBLP DOI BibTeX RDF |
|
31 | Jason Hickey, Aleksey Nogin, Xin Yu, Alexei Kopylov |
Mechanized meta-reasoning using a hybrid HOAS/de bruijn representation and reflection. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ICFP ![In: Proceedings of the 11th ACM SIGPLAN International Conference on Functional Programming, ICFP 2006, Portland, Oregon, USA, September 16-21, 2006, pp. 172-183, 2006, ACM, 1-59593-309-3. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
languages with bindings, mechanized reasoning, meta-theory, metaPRL, nuPRL, reflection, type theory, higher-order abstract syntax |
28 | Mark Bickford, Dexter Kozen, Alexandra Silva 0001 |
Formalizing Moessner's theorem and generalizations in Nuprl. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Log. Algebraic Methods Program. ![In: J. Log. Algebraic Methods Program. 124, pp. 100713, 2022. The full citation details ...](Pics/full.jpeg) |
2022 |
DBLP DOI BibTeX RDF |
|
28 | Mark Bickford |
Formalizing Category Theory and Presheaf Models of Type Theory in Nuprl. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/1806.06114, 2018. The full citation details ...](Pics/full.jpeg) |
2018 |
DBLP BibTeX RDF |
|
28 | Vincent Rahli |
Exercising Nuprl's Open-Endedness. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ICMS ![In: Mathematical Software - ICMS 2016 - 5th International Conference, Berlin, Germany, July 11-14, 2016, Proceedings, pp. 18-27, 2016, Springer, 978-3-319-42431-6. The full citation details ...](Pics/full.jpeg) |
2016 |
DBLP DOI BibTeX RDF |
|
28 | Vincent Rahli, Mark Bickford, Abhishek Anand |
Formal Program Optimization in Nuprl Using Computational Equivalence and Partial Types. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ITP ![In: Interactive Theorem Proving - 4th International Conference, ITP 2013, Rennes, France, July 22-26, 2013. Proceedings, pp. 261-278, 2013, Springer, 978-3-642-39633-5. The full citation details ...](Pics/full.jpeg) |
2013 |
DBLP DOI BibTeX RDF |
|
28 | Christoph Kreitz |
Nuprl as Logical Framework for Automating Proofs in Category Theory. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Logic and Program Semantics ![In: Logic and Program Semantics - Essays Dedicated to Dexter Kozen on the Occasion of His 60th Birthday, pp. 124-148, 2012, Springer, 978-3-642-29484-6. The full citation details ...](Pics/full.jpeg) |
2012 |
DBLP DOI BibTeX RDF |
|
28 | Stuart F. Allen, Mark Bickford, Robert L. Constable, Richard Eaton, Christoph Kreitz, Lori Lorigo, E. Moran |
Innovations in computational type theory using Nuprl. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Appl. Log. ![In: J. Appl. Log. 4(4), pp. 428-469, 2006. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
|
28 | Paul B. Jackson |
Nuprl. ![Search on Bibsonomy](Pics/bibsonomy.png) |
The Seventeen Provers of the World ![In: The Seventeen Provers of the World, Foreword by Dana S. Scott, pp. 116-126, 2006, Springer, 3-540-30704-4. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
|
28 | Eli Barzilay |
Implementing Reflection in Nuprl. ![Search on Bibsonomy](Pics/bibsonomy.png) |
|
2006 |
RDF |
|
28 | Christoph Kreitz |
Building reliable, high-performance networks with the Nuprl proof development system. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Funct. Program. ![In: J. Funct. Program. 14(1), pp. 21-68, 2004. The full citation details ...](Pics/full.jpeg) |
2004 |
DBLP DOI BibTeX RDF |
|
28 | Ralph Benzinger |
Automated complexity analysis of Nuprl extracted programs Journal of Functional Programming. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Funct. Program. ![In: J. Funct. Program. 11(1), pp. 3-31, 2001. The full citation details ...](Pics/full.jpeg) |
2001 |
DBLP DOI BibTeX RDF |
|
28 | Ralph Benzinger |
Automated Complexity Analysis of NuPRL Extracts. ![Search on Bibsonomy](Pics/bibsonomy.png) |
|
2001 |
RDF |
|
28 | Mark Bickford, Jason Hickey |
Predicate Transformers for Infinite-State Automata in NuPRL Type Theory. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IWFM ![In: 3rd Irish Workshop on Formal Methods, Galway, Ireland, July 1999, 1999, BCS. The full citation details ...](Pics/full.jpeg) |
1999 |
DBLP BibTeX RDF |
|
28 | Pavel Naumov |
Formalizing Reference Types in NuPRL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
|
1998 |
RDF |
|
28 | Jason J. Hickey |
Nuprl-Light: An Implementation Framework for Higher-Order Logics. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CADE ![In: Automated Deduction - CADE-14, 14th International Conference on Automated Deduction, Townsville, North Queensland, Australia, July 13-17, 1997, Proceedings, pp. 395-399, 1997, Springer, 3-540-63104-6. The full citation details ...](Pics/full.jpeg) |
1997 |
DBLP DOI BibTeX RDF |
|
28 | Roderick Moten |
Concurrent Refinement in Nuprl. ![Search on Bibsonomy](Pics/bibsonomy.png) |
|
1997 |
RDF |
|
28 | Douglas J. Howe |
Importing Mathematics from HOL into Nuprl. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 9th International Conference, TPHOLs'96, Turku, Finland, August 26-30, 1996, Proceedings, pp. 267-281, 1996, Springer, 3-540-61587-3. The full citation details ...](Pics/full.jpeg) |
1996 |
DBLP DOI BibTeX RDF |
|
28 | Douglas J. Howe |
Semantic Foundations for Embedding HOL in Nuprl. ![Search on Bibsonomy](Pics/bibsonomy.png) |
AMAST ![In: Algebraic Methodology and Software Technology, 5th International Conference, AMAST '96, Munich, Germany, July 1-5, 1996, Proceedings, pp. 85-101, 1996, Springer, 3-540-61463-X. The full citation details ...](Pics/full.jpeg) |
1996 |
DBLP DOI BibTeX RDF |
|
28 | Roderick Moten |
Nuprl as a concurrent interactive theorem prover. ![Search on Bibsonomy](Pics/bibsonomy.png) |
African Americans in Mathematics ![In: African Americans in Mathematics, Proceedings of a DIMACS Workshop, Piscataway, New Jersey, USA, June 26-28, 1996, pp. 149-154, 1996, DIMACS/AMS, 978-0-8218-1142-9. The full citation details ...](Pics/full.jpeg) |
1996 |
DBLP DOI BibTeX RDF |
|
28 | Paul B. Jackson |
Enhancing the NUPRL Proof Development System and Applying it to Computational Abstract Algebra. ![Search on Bibsonomy](Pics/bibsonomy.png) |
|
1995 |
RDF |
|
28 | Douglas J. Howe |
Reasoning About Functional Programs in Nuprl. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Functional Programming, Concurrency, Simulation and Automated Reasoning ![In: Functional Programming, Concurrency, Simulation and Automated Reasoning: International Lecture Series 1991-1992, McMaster University, Hamilton, Ontario, Canada, pp. 145-164, 1993, Springer, 3-540-56883-2. The full citation details ...](Pics/full.jpeg) |
1993 |
DBLP DOI BibTeX RDF |
|
28 | Wilfred Z. Chen |
Tactic-based Theorem Proving and Knowledge-based Forward Chaining: an Experiment with Nuprl and Ontic. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CADE ![In: Automated Deduction - CADE-11, 11th International Conference on Automated Deduction, Saratoga Springs, NY, USA, June 15-18, 1992, Proceedings, pp. 552-566, 1992, Springer, 3-540-55602-8. The full citation details ...](Pics/full.jpeg) |
1992 |
DBLP DOI BibTeX RDF |
|
28 | Paul B. Jackson |
Nuprl and Its Use in Circuit Design. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPCD ![In: Theorem Provers in Circuit Design, Proceedings of the IFIP TC10/WG 10.2 International Conference on Theorem Provers in Circuit Design: Theory, Practice and Experience, Nijmegen, The Netherlands, 22-24 June 1992, Proceedings, pp. 311-336, 1992, North-Holland, 0-444-89686-4. The full citation details ...](Pics/full.jpeg) |
1992 |
DBLP BibTeX RDF |
|
28 | Robert L. Constable, Stuart F. Allen, Mark Bromley, Rance Cleaveland, J. F. Cremer, Robert Harper 0001, Douglas J. Howe, Todd B. Knoblock, Nax Paul Mendler, Prakash Panangaden, James T. Sasaki, Scott F. Smith 0001 |
Implementing mathematics with the Nuprl proof development system. ![Search on Bibsonomy](Pics/bibsonomy.png) |
|
1986 |
RDF |
|
17 | Mark Bickford |
Unguessable Atoms: A Logical Foundation for Security. ![Search on Bibsonomy](Pics/bibsonomy.png) |
VSTTE ![In: Verified Software: Theories, Tools, Experiments, Second International Conference, VSTTE 2008, Toronto, Canada, October 6-9, 2008. Proceedings, pp. 30-53, 2008, Springer, 978-3-540-87872-8. The full citation details ...](Pics/full.jpeg) |
2008 |
DBLP DOI BibTeX RDF |
|
17 | Mike Gordon |
Twenty Years of Theorem Proving for HOLs Past, Present and Future. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 21st International Conference, TPHOLs 2008, Montreal, Canada, August 18-21, 2008. Proceedings, pp. 1-5, 2008, Springer, 978-3-540-71065-3. The full citation details ...](Pics/full.jpeg) |
2008 |
DBLP DOI BibTeX RDF |
|
17 | Claudio Sacerdoti Coen |
A Semi-reflexive Tactic for (Sub-)Equational Reasoning. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TYPES ![In: Types for Proofs and Programs, International Workshop, TYPES 2004, Jouy-en-Josas, France, December 15-18, 2004, Revised Selected Papers, pp. 98-114, 2004, Springer, 3-540-31428-8. The full citation details ...](Pics/full.jpeg) |
2004 |
DBLP DOI BibTeX RDF |
|
17 | Carsten Schürmann |
Twelf and Delphin: Logic and Functional Programming in a Meta-logical Framework. ![Search on Bibsonomy](Pics/bibsonomy.png) |
FLOPS ![In: Functional and Logic Programming, 7th International Symposium, FLOPS 2004, Nara, Japan, April 7-9, 2004, Proceedings, pp. 22-23, 2004, Springer, 3-540-21402-X. The full citation details ...](Pics/full.jpeg) |
2004 |
DBLP DOI BibTeX RDF |
|
17 | Claudio Sacerdoti Coen |
From Proof-Assistants to Distributed Libraries of Mathematics: Tips and Pitfalls. ![Search on Bibsonomy](Pics/bibsonomy.png) |
MKM ![In: Mathematical Knowledge Management, Second International Conference, MKM 2003, Bertinoro, Italy, February 16-18, 2003, Proceedings, pp. 30-44, 2003, Springer, 3-540-00568-4. The full citation details ...](Pics/full.jpeg) |
2003 |
DBLP DOI BibTeX RDF |
|
17 | Ming-Yuan Zhu, Lei Luo 0004, Guang-Zhe Xiong |
The Minimal Model of Operating Systems. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACM SIGOPS Oper. Syst. Rev. ![In: ACM SIGOPS Oper. Syst. Rev. 35(3), pp. 22-29, 2001. The full citation details ...](Pics/full.jpeg) |
2001 |
DBLP DOI BibTeX RDF |
|
17 | Ming-Yuan Zhu, Lei Luo 0004, Guang-Zhe Xiong |
A Provably Correct Operating System: delta-Core. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACM SIGOPS Oper. Syst. Rev. ![In: ACM SIGOPS Oper. Syst. Rev. 35(1), pp. 17-33, 2001. The full citation details ...](Pics/full.jpeg) |
2001 |
DBLP DOI BibTeX RDF |
|
17 | Mark Bickford, Christoph Kreitz, Robbert van Renesse, Xiaoming Liu 0003 |
Proving Hybrid Protocols Correct. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 14th International Conference, TPHOLs 2001, Edinburgh, Scotland, UK, September 3-6, 2001, Proceedings, pp. 105-120, 2001, Springer, 3-540-42525-X. The full citation details ...](Pics/full.jpeg) |
2001 |
DBLP DOI BibTeX RDF |
|
17 | Stephan Schmitt, Lori Lorigo, Christoph Kreitz, Aleksey Nogin |
JProver : Integrating Connection-Based Theorem Proving into Interactive Proof Assistants. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IJCAR ![In: Automated Reasoning, First International Joint Conference, IJCAR 2001, Siena, Italy, June 18-23, 2001, Proceedings, pp. 421-426, 2001, Springer, 3-540-42254-4. The full citation details ...](Pics/full.jpeg) |
2001 |
DBLP DOI BibTeX RDF |
|
17 | Amy P. Felty, Douglas J. Howe, Abhik Roychoudhury |
Formal Metatheory using Implicit Syntax, and an Application to Data Abstraction for Asynchronous Systems. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CADE ![In: Automated Deduction - CADE-16, 16th International Conference on Automated Deduction, Trento, Italy, July 7-10, 1999, Proceedings, pp. 237-251, 1999, Springer, 3-540-66222-7. The full citation details ...](Pics/full.jpeg) |
1999 |
DBLP DOI BibTeX RDF |
|
17 | Xiaoming Liu 0003, Christoph Kreitz, Robbert van Renesse, Jason Hickey, Mark Hayden, Kenneth P. Birman, Robert L. Constable |
Building reliable, high-performance communication systems from components. ![Search on Bibsonomy](Pics/bibsonomy.png) |
SOSP ![In: Proceedings of the 17th ACM Symposium on Operating System Principles, SOSP 1999, Kiawah Island Resort, near Charleston, South Carolina, USA, December 12-15, 1999, pp. 80-92, 1999, ACM, 1-58113-140-2. The full citation details ...](Pics/full.jpeg) |
1999 |
DBLP DOI BibTeX RDF |
|
17 | Christoph Kreitz |
Automated Fast-Track Reconfiguration of Group Communication Systems. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TACAS ![In: Tools and Algorithms for Construction and Analysis of Systems, 5th International Conference, TACAS '99, Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS'99, Amsterdam, The Netherlands, March 22-28, 1999, Proceedings, pp. 104-118, 1999, Springer, 3-540-65703-7. The full citation details ...](Pics/full.jpeg) |
1999 |
DBLP DOI BibTeX RDF |
|
17 | Douglas J. Howe |
Interactive Theorem Proving Using Type Theory. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CSL ![In: Computer Science Logic, 13th International Workshop, CSL '99, 8th Annual Conference of the EACSL, Madrid, Spain, September 20-25, 1999, Proceedings, pp. 578, 1999, Springer, 3-540-66536-6. The full citation details ...](Pics/full.jpeg) |
1999 |
DBLP DOI BibTeX RDF |
|
17 | Mark D. Aagaard, Miriam Leeser |
PBS: proven Boolean simplification. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. ![In: IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 13(4), pp. 459-470, 1994. The full citation details ...](Pics/full.jpeg) |
1994 |
DBLP DOI BibTeX RDF |
|
17 | Mark D. Aagaard, Miriam Leeser, Phillip J. Windley |
Toward a Super Duper Hardware Tactic. ![Search on Bibsonomy](Pics/bibsonomy.png) |
HUG ![In: Higher Order Logic Theorem Proving and its Applications, 6th International Workshop, HUG '93, Vancouver, BC, Canada, August 11-13, 1993, Proceedings, pp. 399-412, 1993, Springer, 3-540-57826-9. The full citation details ...](Pics/full.jpeg) |
1993 |
DBLP DOI BibTeX RDF |
|
17 | Thierry Boy de la Tour, Christoph Kreitz |
Building Proofs by Analogy via the Curry-Horward Isomorphism. ![Search on Bibsonomy](Pics/bibsonomy.png) |
LPAR ![In: Logic Programming and Automated Reasoning,International Conference LPAR'92, St. Petersburg, Russia, July 15-20, 1992, Proceedings, pp. 202-213, 1992, Springer, 3-540-55727-X. The full citation details ...](Pics/full.jpeg) |
1992 |
DBLP DOI BibTeX RDF |
|
17 | David A. Basin |
An Environment For Automated Reasoning About Partial Functions. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CADE ![In: 9th International Conference on Automated Deduction, Argonne, Illinois, USA, May 23-26, 1988, Proceedings, pp. 101-110, 1988, Springer, 3-540-19343-X. The full citation details ...](Pics/full.jpeg) |
1988 |
DBLP DOI BibTeX RDF |
Automated program development, unsolvability, theorem proving, computability, type theory, constructivity, tactics, partial functions |