MetaPRL - A Modular Logical Environment

No abstract is available for this paper.

• Publication year

  2003

• Venue

  International Conference on Theorem Proving in Higher Order Logics

• Publication date

  2003-09-08

• Fields of study

  Computer Science

• Identifiers
  DOI 10.1007/10930755_19
• External record

  Open on Semantic Scholar

• Source metadata

  Semantic Scholar

• No claims are published for this paper.

• No concepts are published for this paper.

• FDL: A Prototype Formal Digital Library

  2004cited by this paper
• Automated Theorem Proving

  2004cited by this paper
• Phobos: a front-end approach to extensible compilers

  2003cited by this paper
• Dependent intersection: a new way of defining records in type theory

  2003cited by this paper
• Formalizing Abstract Algebra in Constructive Set Theory

  2003cited by this paper
• Óöññð Óñôôððö Áñôððññòøøøøóò Ò Äóóó Blockin Blockinð Ööññûóöö

  2003cited by this paper
• Formal Design Environments

  2003cited by this paper
• Reflecting Higher-Order Abstract Syntax in Nuprl ?

  2002cited by this paper
• Quotient Types: A Modular Approach

  2002cited by this paper
• Theory and Implementation of an Efficient Tactic-Based Logical Framework

  2002cited by this paper
• Process Migration and Transactions Using a Novel Intermediate Language

  2002cited by this paper
• Sequent Schema for Derived Rules

  2002cited by this paper
• Logical Frameworks

  2001cited by this paper
• Proving Hybrid Protocols Correct

  2001cited by this paper
• JProver : Integrating Connection-Based Theorem Proving into Interactive Proof Assistants

  2001influential reference
• A Tutorial Introduction

  2001cited by this paper
• Markov's Principle for Propositional Type Theory

  2001cited by this paper
• The Nuprl Open Logical Environment

  2000influential reference
• A Uniform Procedure for Converting Matrix Proofs into Sequent-Style Systems

  2000cited by this paper
• Nuprl ’ s Class Theory and its Applications

  2000cited by this paper
• Fast Tactic-Based Theorem Proving

  2000cited by this paper
• Proof General: A Generic Tool for Proof Development

  2000cited by this paper
• The coq proof assistant reference manual

  2000cited by this paper
• The MetaPRL Logical Programming Environment

  2000influential reference
• Building reliable, high-performance communication systems from components

  1999cited by this paper
• Connection-based Theorem Proving in Classical and Non-classical Logics

  1999cited by this paper
• Fault-Tolerant Distributed Theorem Proving

  1999cited by this paper
• Theorem Proving in Higher Order Logics

  1999cited by this paper
• The Ensemble System

  1998cited by this paper
• Constructive Mathematics

  1997cited by this paper
• Proceedings of the 10th International Conference on Theorem Proving in Higher Order Logics

  1997cited by this paper
• Notes on constructive set theory

  1997cited by this paper
• The Coq proof assistant : reference manual, version 6.1

  1997cited by this paper
• Nuprl-Light: An Implementation Framework for Higher-Order Logics

  1997cited by this paper
• Theorem Proving in Higher Order Logics

  1997cited by this paper
• Formal Objects in Type Theory Using Very Dependent Types

  1996cited by this paper
• A Theory of Objects

  1996cited by this paper
• HOL Light: A Tutorial Introduction

  1996cited by this paper
• Enhancing the NUPRL Proof Development System and Applying it to Computational Abstract Algebra

  1995influential reference
• A Notation for Computer Aided Mathematics

  1994cited by this paper
• Isabelle: A Generic Theorem Prover

  1994cited by this paper
• Le langage Caml

  1993cited by this paper
• Isabelle tutorial and user’s manual

  1990cited by this paper
• Automated theorem proving (second revised edition) by Wolfgang Bibel, Vieweg 1987

  1988cited by this paper
• The Type Theoretic Interpretation of Constructive Set Theory: Inductive Definitions

  1986cited by this paper
• Constructive mathematics and computer programming

  1984cited by this paper
• A Logic for Correct Program Development

  1979cited by this paper
• Edinburgh LCF: A mechanised logic of computation

  1979cited by this paper
• Edinburgh lcf: a mechanized logic of computation

  1978cited by this paper
• The Type Theoretic Interpretation of Constructive Set Theory

  1978cited by this paper
• On the theory of programming logics

  1977cited by this paper
• Constructive set theory

  1975cited by this paper

• Mechanizing Synthetic Tait Computability in Istari

  2025cites this paper
• Verifiably Safe Autonomy for Cyber-Physical Systems

  2018cites this paper
• HOL Light QE

  2018influential citation
• Formal Systems, Logics, and Programs

  2017cites this paper
• Bellerophon: Tactical Theorem Proving for Hybrid Systems

  2017cites this paper
• Interactive Theorem Proving: 8th International Conference, ITP 2017, Brasília, Brazil, September 26–29, 2017, Proceedings

  2017cites this paper
• Syntax and Semantics of Abstract Binding Trees

  2016cites this paper
• Object-Oriented Mechanisms for Interoperability between Proof Systems. (Mécanismes Orientés-Objets pour l'Interopérabilité entre Systèmes de Preuve)

  2016cites this paper
• Incorporating Quotation and Evaluation into Church's Type Theory: Syntax and Semantics

  2016cites this paper
• History of Interactive Theorem Proving

  2014cites this paper
• TR-2014001: Computer-Aided Reasoning about Knowledge and Justifications

  2014cites this paper
• TR-2014001: Computer-Aided Reasoning about Knowledge and Justific ations

  2014cites this paper
• Formal Program Optimization in Nuprl Using Computational Equivalence and Partial Types

  2013cites this paper
• Advanced Programming Languages CS6110 Spring 2012

  2012cites this paper
• Russell's Orders in Kripke's Theory of Truth and Computational Type Theory

  2012cites this paper
• Intuitionistic completeness of first-order logic

  2011cites this paper
• The Triumph of Types : Creating a Logic of Computational Reality

  2011influential citation
• The Triumph of Types: Principia Mathematica's Impact on Computer Science

  2011cites this paper
• Faster and More Complete Extended Static Checking for the Java Modeling Language

  2010cites this paper
• A new type for tactics

  2009cites this paper
• Computational type theory

  2009cites this paper
• Invariants for the FoCaL language

  2009cites this paper
• Computer-Aided Reasoning about Knowledge and Justifications

  2009cites this paper
• A new type for tactics A new type for tactics

  2009influential citation
• Data Compression for Proof Replay

  2008cites this paper
• Czech clitics in higher order grammar

  2007cites this paper
• Reflection and Its Application to Mechanized MetaReasoning About Programming Languages

  2007cites this paper
• Practical Reflection for Sequent Logics

  2007cites this paper
• Publication/Citation: A Proof-Theoretic Approach to Mathematical Knowledge Management

  2007influential citation
• ILC: A Foundation for Automated Reasoning About Pointer Programs

  2006cites this paper
• A Computation Infrastructure for Knowledge-Based Development of Reliable Software Systems

  2006cites this paper
• Mechanized meta-reasoning using a hybrid HOAS/de bruijn representation and reflection

  2006cites this paper
• Enabling Large Scale Coherency Among Mathematical Texts

  2006cites this paper
• Innovations in computational type theory using Nuprl

  2006influential citation
• Extracting Programs from Constructive HOL Proofs via IZF Set-Theoretic Semantics

  2006cites this paper
• Formal compiler construction in a logical framework

  2006cites this paper
• The SAD System: Deductive Assistance in an Intelligent Linguistic Environment

  2006cites this paper
• The 2006 Federated Logic Conference

  2006cites this paper
• Formalizing Type Operations Using the "Image" Type Constructor

  2006cites this paper
• Using Formal Reference to Enhance Authority and Integrity in Online Mathematical Texts

  2006cites this paper
• Integration of decision procedures into high-order interactive provers

  2006cites this paper
• KAT-ML: an interactive theorem prover for Kleene algebra with tests

  2006cites this paper
• IMPLEMENTING DIRECT REFLECTION IN NUPRL

  2006influential citation
• A computational approach to reflective meta-reasoning about languages with bindings

  2005cites this paper
• Axiomatic Constructor Classes in Isabelle/HOLCF

  2005cites this paper
• Implementing Reflection in Nuprl

  2005influential citation
• High-Confidence, Modular Compiler Development in a Formal Environment

  2005cites this paper
• A Decision Procedure for Equational Reasoning in Commutative Algebraic Structures

  2004cites this paper
• TR-2004004: Implementing and Automating Basic Number Theory in MetaPRL Proof Assistant

  2004cites this paper
• A formal reduction for lock-free parallel algorithms

  2004cites this paper
• Building Extensible Compilers in a Formal Framework ? A Formal Framework User ’ s Perspective

  2004cites this paper
• Hierarchical Reflection

  2004cites this paper
• Extensible Hierarchical Tactic Construction in a Logical Framework

  2004cites this paper
• Reliable Frameworks for Extensible Compilers ∗

  2004cites this paper
• Shape Analysis Quantitative Shape Analysis

  2004cites this paper
• Type Theoretical Foundations for Data Structures, Classes, and Objects

  2004cites this paper
• Expressing and Implementing the Computational Content Implicit in Smullyan's Account of Boolean Valuations

  2004cites this paper
• Compiler implementation in a formal logical framework

  2003cites this paper
• Building Reliable Compilers with a Formal Methods Framework

  2003cites this paper
• Formalizing Abstract Algebra in Type Theory with Dependent Records

  2003cites this paper
• Information-intensive Proof Technology Contents 1 Series Introduction and Basics 4

  2003cites this paper
• Formal Compiler Implementation in a Logical Framework

  2003cites this paper
• Theory and Implementation of an Efficient Tactic-Based Logical Framework

  2002cites this paper
• Formal Compiler Construction in a Logical Framework

  year unknowncites this paper
• Lecture 26 – Constructive Type Theory Continued

  year unknowncites this paper