The FacetedDBLP logo    Search for: in:

Disable automatic phrases ?     Syntactic query expansion: ?

Searching for nuPRL with no syntactic query expansion in all metadata.

Publication years (Num. hits)
1986-1994 (15) 1995-1998 (16) 1999-2003 (15) 2004-2016 (15) 2018-2022 (2)
Publication types (Num. hits)
article(9) book(1) incollection(1) inproceedings(47) phdthesis(5)
Venues (Conferences, Journals, ...)
GrowBag graphs for keyword ? (Num. hits/coverage)

Group by:
The graphs summarize 27 occurrences of 18 keywords

Results
Found 63 publication records. Showing 63 according to the selection in the facets
Hits ? Authors Title Venue Year Link Author keywords
97Amy P. Felty, Douglas J. Howe, Frank A. Stomp Protocol Verification in Nuprl. Search on Bibsonomy CAV The full citation details ... 1998 DBLP  DOI  BibTeX  RDF
97Douglas J. Howe A Type Annotation Scheme for Nuprl. Search on Bibsonomy TPHOLs The full citation details ... 1998 DBLP  DOI  BibTeX  RDF
97Douglas J. Howe Computational Metatheory in Nuprl. Search on Bibsonomy CADE The full citation details ... 1988 DBLP  DOI  BibTeX  RDF formal metamathematics, reflection, Theorem proving, type theory, constructive mathematics, tactics
83James L. Caldwell Moving Proofs-As-Programs into Practice. Search on Bibsonomy ASE The full citation details ... 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
79Pavel Naumov, Mark-Oliver Stehr, José Meseguer 0001 The HOL/NuPRL Proof Translator (A Practical Approach to Formal Interoperability). Search on Bibsonomy TPHOLs The full citation details ... 2001 DBLP  DOI  BibTeX  RDF
79Mark D. Aagaard, Miriam Leeser Verifying a Logic Synthesis Tool in Nuprl: A Case Study in Software Verification. Search on Bibsonomy CAV The full citation details ... 1992 DBLP  DOI  BibTeX  RDF
69Robert L. Constable ML Programming in Constructive Type Theory (abstract). Search on Bibsonomy TPHOLs The full citation details ... 1997 DBLP  DOI  BibTeX  RDF
62Carsten Schürmann, Mark-Oliver Stehr An Executable Formalization of the HOL/Nuprl Connection in the Metalogical Framework Twelf. Search on Bibsonomy LPAR The full citation details ... 2006 DBLP  DOI  BibTeX  RDF
62Stuart F. Allen, Robert L. Constable, Richard Eaton, Christoph Kreitz, Lori Lorigo The Nuprl Open Logical Environment. Search on Bibsonomy CADE The full citation details ... 2000 DBLP  DOI  BibTeX  RDF
62James L. Caldwell Classical Propositional Decidability via Nuprl Proof Extraction. Search on Bibsonomy TPHOLs The full citation details ... 1998 DBLP  DOI  BibTeX  RDF
62David A. Basin, Peter Del Vecchio Verification Of Combinational Logic in Nuprl. Search on Bibsonomy Hardware Specification, Verification and Synthesis The full citation details ... 1989 DBLP  DOI  BibTeX  RDF
52Mark Bickford, Robert L. Constable, Joseph Y. Halpern, Sabina Petride Knowledge-Based Synthesis of Distributed Systems Using Event Structures. Search on Bibsonomy LPAR The full citation details ... 2004 DBLP  DOI  BibTeX  RDF
52Mark D. Aagaard, Miriam Leeser Verifying a Logic-Synthesis Algorithm and Implementation: A Case Study in Software Verification. Search on Bibsonomy IEEE Trans. Software Eng. The full citation details ... 1995 DBLP  DOI  BibTeX  RDF weak division, theorem proving, logic synthesis, Software verification, hardware verification
52Paul B. Jackson Exploring Abstract Algebra in Constructive Type Theory. Search on Bibsonomy CADE The full citation details ... 1994 DBLP  DOI  BibTeX  RDF
48Aleksey Nogin, Alexei Kopylov, Xin Yu, Jason Hickey A computational approach to reflective meta-reasoning about languages with bindings. Search on Bibsonomy MERLIN The full citation details ... 2005 DBLP  DOI  BibTeX  RDF MetaPRL, Nuprl, languages with bindings, programming language, reflection, experimentation, type theory, higher-order abstract syntax
45James L. Caldwell Extracting General Recursive Program Schemes in Nuprl's Type Theory. Search on Bibsonomy LOPSTR The full citation details ... 2001 DBLP  DOI  BibTeX  RDF
45Amy P. Felty, Douglas J. Howe Hybrid Interactive Theorem Proving Using Nuprl and HOL. Search on Bibsonomy CADE The full citation details ... 1997 DBLP  DOI  BibTeX  RDF
45David A. Basin Building Theories in Nuprl. Search on Bibsonomy Logic at Botik The full citation details ... 1989 DBLP  DOI  BibTeX  RDF
45Douglas J. Howe Implementing Number Theory: An Experiment with Nuprl. Search on Bibsonomy CADE The full citation details ... 1986 DBLP  DOI  BibTeX  RDF
35Roderick Moten Exploiting Parallelism in Interactive Theorem Provers. Search on Bibsonomy TPHOLs The full citation details ... 1998 DBLP  DOI  BibTeX  RDF
35Christoph Kreitz, Mark Hayden, Jason Hickey A Proof Environment for the Development of Group Communication Systems. Search on Bibsonomy CADE The full citation details ... 1998 DBLP  DOI  BibTeX  RDF
35James A. Altucher, Prakash Panangaden A Mechanically Assisted Constructive Proof in Category Theory. Search on Bibsonomy CADE The full citation details ... 1990 DBLP  DOI  BibTeX  RDF
31Jason Hickey, Aleksey Nogin, Xin Yu, Alexei Kopylov Mechanized meta-reasoning using a hybrid HOAS/de bruijn representation and reflection. Search on Bibsonomy ICFP The full citation details ... 2006 DBLP  DOI  BibTeX  RDF languages with bindings, mechanized reasoning, meta-theory, metaPRL, nuPRL, reflection, type theory, higher-order abstract syntax
28Mark Bickford, Dexter Kozen, Alexandra Silva 0001 Formalizing Moessner's theorem and generalizations in Nuprl. Search on Bibsonomy J. Log. Algebraic Methods Program. The full citation details ... 2022 DBLP  DOI  BibTeX  RDF
28Mark Bickford Formalizing Category Theory and Presheaf Models of Type Theory in Nuprl. Search on Bibsonomy CoRR The full citation details ... 2018 DBLP  BibTeX  RDF
28Vincent Rahli Exercising Nuprl's Open-Endedness. Search on Bibsonomy ICMS The full citation details ... 2016 DBLP  DOI  BibTeX  RDF
28Vincent Rahli, Mark Bickford, Abhishek Anand Formal Program Optimization in Nuprl Using Computational Equivalence and Partial Types. Search on Bibsonomy ITP The full citation details ... 2013 DBLP  DOI  BibTeX  RDF
28Christoph Kreitz Nuprl as Logical Framework for Automating Proofs in Category Theory. Search on Bibsonomy Logic and Program Semantics The full citation details ... 2012 DBLP  DOI  BibTeX  RDF
28Stuart 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 J. Appl. Log. The full citation details ... 2006 DBLP  DOI  BibTeX  RDF
28Paul B. Jackson Nuprl. Search on Bibsonomy The Seventeen Provers of the World The full citation details ... 2006 DBLP  DOI  BibTeX  RDF
28Eli Barzilay Implementing Reflection in Nuprl. Search on Bibsonomy 2006   RDF
28Christoph Kreitz Building reliable, high-performance networks with the Nuprl proof development system. Search on Bibsonomy J. Funct. Program. The full citation details ... 2004 DBLP  DOI  BibTeX  RDF
28Ralph Benzinger Automated complexity analysis of Nuprl extracted programs Journal of Functional Programming. Search on Bibsonomy J. Funct. Program. The full citation details ... 2001 DBLP  DOI  BibTeX  RDF
28Ralph Benzinger Automated Complexity Analysis of NuPRL Extracts. Search on Bibsonomy 2001   RDF
28Mark Bickford, Jason Hickey Predicate Transformers for Infinite-State Automata in NuPRL Type Theory. Search on Bibsonomy IWFM The full citation details ... 1999 DBLP  BibTeX  RDF
28Pavel Naumov Formalizing Reference Types in NuPRL. Search on Bibsonomy 1998   RDF
28Jason J. Hickey Nuprl-Light: An Implementation Framework for Higher-Order Logics. Search on Bibsonomy CADE The full citation details ... 1997 DBLP  DOI  BibTeX  RDF
28Roderick Moten Concurrent Refinement in Nuprl. Search on Bibsonomy 1997   RDF
28Douglas J. Howe Importing Mathematics from HOL into Nuprl. Search on Bibsonomy TPHOLs The full citation details ... 1996 DBLP  DOI  BibTeX  RDF
28Douglas J. Howe Semantic Foundations for Embedding HOL in Nuprl. Search on Bibsonomy AMAST The full citation details ... 1996 DBLP  DOI  BibTeX  RDF
28Roderick Moten Nuprl as a concurrent interactive theorem prover. Search on Bibsonomy African Americans in Mathematics The full citation details ... 1996 DBLP  DOI  BibTeX  RDF
28Paul B. Jackson Enhancing the NUPRL Proof Development System and Applying it to Computational Abstract Algebra. Search on Bibsonomy 1995   RDF
28Douglas J. Howe Reasoning About Functional Programs in Nuprl. Search on Bibsonomy Functional Programming, Concurrency, Simulation and Automated Reasoning The full citation details ... 1993 DBLP  DOI  BibTeX  RDF
28Wilfred Z. Chen Tactic-based Theorem Proving and Knowledge-based Forward Chaining: an Experiment with Nuprl and Ontic. Search on Bibsonomy CADE The full citation details ... 1992 DBLP  DOI  BibTeX  RDF
28Paul B. Jackson Nuprl and Its Use in Circuit Design. Search on Bibsonomy TPCD The full citation details ... 1992 DBLP  BibTeX  RDF
28Robert 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 1986   RDF
17Mark Bickford Unguessable Atoms: A Logical Foundation for Security. Search on Bibsonomy VSTTE The full citation details ... 2008 DBLP  DOI  BibTeX  RDF
17Mike Gordon Twenty Years of Theorem Proving for HOLs Past, Present and Future. Search on Bibsonomy TPHOLs The full citation details ... 2008 DBLP  DOI  BibTeX  RDF
17Claudio Sacerdoti Coen A Semi-reflexive Tactic for (Sub-)Equational Reasoning. Search on Bibsonomy TYPES The full citation details ... 2004 DBLP  DOI  BibTeX  RDF
17Carsten Schürmann Twelf and Delphin: Logic and Functional Programming in a Meta-logical Framework. Search on Bibsonomy FLOPS The full citation details ... 2004 DBLP  DOI  BibTeX  RDF
17Claudio Sacerdoti Coen From Proof-Assistants to Distributed Libraries of Mathematics: Tips and Pitfalls. Search on Bibsonomy MKM The full citation details ... 2003 DBLP  DOI  BibTeX  RDF
17Ming-Yuan Zhu, Lei Luo 0004, Guang-Zhe Xiong The Minimal Model of Operating Systems. Search on Bibsonomy ACM SIGOPS Oper. Syst. Rev. The full citation details ... 2001 DBLP  DOI  BibTeX  RDF
17Ming-Yuan Zhu, Lei Luo 0004, Guang-Zhe Xiong A Provably Correct Operating System: delta-Core. Search on Bibsonomy ACM SIGOPS Oper. Syst. Rev. The full citation details ... 2001 DBLP  DOI  BibTeX  RDF
17Mark Bickford, Christoph Kreitz, Robbert van Renesse, Xiaoming Liu 0003 Proving Hybrid Protocols Correct. Search on Bibsonomy TPHOLs The full citation details ... 2001 DBLP  DOI  BibTeX  RDF
17Stephan Schmitt, Lori Lorigo, Christoph Kreitz, Aleksey Nogin JProver : Integrating Connection-Based Theorem Proving into Interactive Proof Assistants. Search on Bibsonomy IJCAR The full citation details ... 2001 DBLP  DOI  BibTeX  RDF
17Amy P. Felty, Douglas J. Howe, Abhik Roychoudhury Formal Metatheory using Implicit Syntax, and an Application to Data Abstraction for Asynchronous Systems. Search on Bibsonomy CADE The full citation details ... 1999 DBLP  DOI  BibTeX  RDF
17Xiaoming 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 SOSP The full citation details ... 1999 DBLP  DOI  BibTeX  RDF
17Christoph Kreitz Automated Fast-Track Reconfiguration of Group Communication Systems. Search on Bibsonomy TACAS The full citation details ... 1999 DBLP  DOI  BibTeX  RDF
17Douglas J. Howe Interactive Theorem Proving Using Type Theory. Search on Bibsonomy CSL The full citation details ... 1999 DBLP  DOI  BibTeX  RDF
17Mark D. Aagaard, Miriam Leeser PBS: proven Boolean simplification. Search on Bibsonomy IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. The full citation details ... 1994 DBLP  DOI  BibTeX  RDF
17Mark D. Aagaard, Miriam Leeser, Phillip J. Windley Toward a Super Duper Hardware Tactic. Search on Bibsonomy HUG The full citation details ... 1993 DBLP  DOI  BibTeX  RDF
17Thierry Boy de la Tour, Christoph Kreitz Building Proofs by Analogy via the Curry-Horward Isomorphism. Search on Bibsonomy LPAR The full citation details ... 1992 DBLP  DOI  BibTeX  RDF
17David A. Basin An Environment For Automated Reasoning About Partial Functions. Search on Bibsonomy CADE The full citation details ... 1988 DBLP  DOI  BibTeX  RDF Automated program development, unsolvability, theorem proving, computability, type theory, constructivity, tactics, partial functions
Displaying result #1 - #63 of 63 (100 per page; Change: )
Valid XHTML 1.1! Valid CSS! [Valid RSS]
Maintained by L3S.
Previously maintained by Jörg Diederich.
Based upon DBLP by Michael Ley.
open data data released under the ODC-BY 1.0 license