Search results for "nuPRL"

Hits ?▲	Authors	Title	Venue	Year	Link	Author keywords
97	Amy P. Felty, Douglas J. Howe, Frank A. Stomp	Protocol Verification in Nuprl.	CAV	1998	DBLP DOI BibTeX RDF
97	Douglas J. Howe	A Type Annotation Scheme for Nuprl.	TPHOLs	1998	DBLP DOI BibTeX RDF
97	Douglas J. Howe	Computational Metatheory in Nuprl.	CADE	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.	ASE	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).	TPHOLs	2001	DBLP DOI BibTeX RDF
79	Mark D. Aagaard, Miriam Leeser	Verifying a Logic Synthesis Tool in Nuprl: A Case Study in Software Verification.	CAV	1992	DBLP DOI BibTeX RDF
69	Robert L. Constable	ML Programming in Constructive Type Theory (abstract).	TPHOLs	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.	LPAR	2006	DBLP DOI BibTeX RDF
62	Stuart F. Allen, Robert L. Constable, Richard Eaton, Christoph Kreitz, Lori Lorigo	The Nuprl Open Logical Environment.	CADE	2000	DBLP DOI BibTeX RDF
62	James L. Caldwell	Classical Propositional Decidability via Nuprl Proof Extraction.	TPHOLs	1998	DBLP DOI BibTeX RDF
62	David A. Basin, Peter Del Vecchio	Verification Of Combinational Logic in Nuprl.	Hardware Specification, Verification and Synthesis	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.	LPAR	2004	DBLP DOI BibTeX RDF
52	Mark D. Aagaard, Miriam Leeser	Verifying a Logic-Synthesis Algorithm and Implementation: A Case Study in Software Verification.	IEEE Trans. Software Eng.	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.	CADE	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.	MERLIN	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.	LOPSTR	2001	DBLP DOI BibTeX RDF
45	Amy P. Felty, Douglas J. Howe	Hybrid Interactive Theorem Proving Using Nuprl and HOL.	CADE	1997	DBLP DOI BibTeX RDF
45	David A. Basin	Building Theories in Nuprl.	Logic at Botik	1989	DBLP DOI BibTeX RDF
45	Douglas J. Howe	Implementing Number Theory: An Experiment with Nuprl.	CADE	1986	DBLP DOI BibTeX RDF
35	Roderick Moten	Exploiting Parallelism in Interactive Theorem Provers.	TPHOLs	1998	DBLP DOI BibTeX RDF
35	Christoph Kreitz, Mark Hayden, Jason Hickey	A Proof Environment for the Development of Group Communication Systems.	CADE	1998	DBLP DOI BibTeX RDF
35	James A. Altucher, Prakash Panangaden	A Mechanically Assisted Constructive Proof in Category Theory.	CADE	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.	ICFP	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.	J. Log. Algebraic Methods Program.	2022	DBLP DOI BibTeX RDF
28	Mark Bickford	Formalizing Category Theory and Presheaf Models of Type Theory in Nuprl.	CoRR	2018	DBLP BibTeX RDF
28	Vincent Rahli	Exercising Nuprl's Open-Endedness.	ICMS	2016	DBLP DOI BibTeX RDF
28	Vincent Rahli, Mark Bickford, Abhishek Anand	Formal Program Optimization in Nuprl Using Computational Equivalence and Partial Types.	ITP	2013	DBLP DOI BibTeX RDF
28	Christoph Kreitz	Nuprl as Logical Framework for Automating Proofs in Category Theory.	Logic and Program Semantics	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.	J. Appl. Log.	2006	DBLP DOI BibTeX RDF
28	Paul B. Jackson	Nuprl.	The Seventeen Provers of the World	2006	DBLP DOI BibTeX RDF
28	Eli Barzilay	Implementing Reflection in Nuprl.		2006	RDF
28	Christoph Kreitz	Building reliable, high-performance networks with the Nuprl proof development system.	J. Funct. Program.	2004	DBLP DOI BibTeX RDF
28	Ralph Benzinger	Automated complexity analysis of Nuprl extracted programs Journal of Functional Programming.	J. Funct. Program.	2001	DBLP DOI BibTeX RDF
28	Ralph Benzinger	Automated Complexity Analysis of NuPRL Extracts.		2001	RDF
28	Mark Bickford, Jason Hickey	Predicate Transformers for Infinite-State Automata in NuPRL Type Theory.	IWFM	1999	DBLP BibTeX RDF
28	Pavel Naumov	Formalizing Reference Types in NuPRL.		1998	RDF
28	Jason J. Hickey	Nuprl-Light: An Implementation Framework for Higher-Order Logics.	CADE	1997	DBLP DOI BibTeX RDF
28	Roderick Moten	Concurrent Refinement in Nuprl.		1997	RDF
28	Douglas J. Howe	Importing Mathematics from HOL into Nuprl.	TPHOLs	1996	DBLP DOI BibTeX RDF
28	Douglas J. Howe	Semantic Foundations for Embedding HOL in Nuprl.	AMAST	1996	DBLP DOI BibTeX RDF
28	Roderick Moten	Nuprl as a concurrent interactive theorem prover.	African Americans in Mathematics	1996	DBLP DOI BibTeX RDF
28	Paul B. Jackson	Enhancing the NUPRL Proof Development System and Applying it to Computational Abstract Algebra.		1995	RDF
28	Douglas J. Howe	Reasoning About Functional Programs in Nuprl.	Functional Programming, Concurrency, Simulation and Automated Reasoning	1993	DBLP DOI BibTeX RDF
28	Wilfred Z. Chen	Tactic-based Theorem Proving and Knowledge-based Forward Chaining: an Experiment with Nuprl and Ontic.	CADE	1992	DBLP DOI BibTeX RDF
28	Paul B. Jackson	Nuprl and Its Use in Circuit Design.	TPCD	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.		1986	RDF
17	Mark Bickford	Unguessable Atoms: A Logical Foundation for Security.	VSTTE	2008	DBLP DOI BibTeX RDF
17	Mike Gordon	Twenty Years of Theorem Proving for HOLs Past, Present and Future.	TPHOLs	2008	DBLP DOI BibTeX RDF
17	Claudio Sacerdoti Coen	A Semi-reflexive Tactic for (Sub-)Equational Reasoning.	TYPES	2004	DBLP DOI BibTeX RDF
17	Carsten Schürmann	Twelf and Delphin: Logic and Functional Programming in a Meta-logical Framework.	FLOPS	2004	DBLP DOI BibTeX RDF
17	Claudio Sacerdoti Coen	From Proof-Assistants to Distributed Libraries of Mathematics: Tips and Pitfalls.	MKM	2003	DBLP DOI BibTeX RDF
17	Ming-Yuan Zhu, Lei Luo 0004, Guang-Zhe Xiong	The Minimal Model of Operating Systems.	ACM SIGOPS Oper. Syst. Rev.	2001	DBLP DOI BibTeX RDF
17	Ming-Yuan Zhu, Lei Luo 0004, Guang-Zhe Xiong	A Provably Correct Operating System: delta-Core.	ACM SIGOPS Oper. Syst. Rev.	2001	DBLP DOI BibTeX RDF
17	Mark Bickford, Christoph Kreitz, Robbert van Renesse, Xiaoming Liu 0003	Proving Hybrid Protocols Correct.	TPHOLs	2001	DBLP DOI BibTeX RDF
17	Stephan Schmitt, Lori Lorigo, Christoph Kreitz, Aleksey Nogin	JProver : Integrating Connection-Based Theorem Proving into Interactive Proof Assistants.	IJCAR	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.	CADE	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.	SOSP	1999	DBLP DOI BibTeX RDF
17	Christoph Kreitz	Automated Fast-Track Reconfiguration of Group Communication Systems.	TACAS	1999	DBLP DOI BibTeX RDF
17	Douglas J. Howe	Interactive Theorem Proving Using Type Theory.	CSL	1999	DBLP DOI BibTeX RDF
17	Mark D. Aagaard, Miriam Leeser	PBS: proven Boolean simplification.	IEEE Trans. Comput. Aided Des. Integr. Circuits Syst.	1994	DBLP DOI BibTeX RDF
17	Mark D. Aagaard, Miriam Leeser, Phillip J. Windley	Toward a Super Duper Hardware Tactic.	HUG	1993	DBLP DOI BibTeX RDF
17	Thierry Boy de la Tour, Christoph Kreitz	Building Proofs by Analogy via the Curry-Horward Isomorphism.	LPAR	1992	DBLP DOI BibTeX RDF
17	David A. Basin	An Environment For Automated Reasoning About Partial Functions.	CADE	1988	DBLP DOI BibTeX RDF	Automated program development, unsolvability, theorem proving, computability, type theory, constructivity, tactics, partial functions