Innovations in computational type theory using Nuprl

DOI10.1016/J.JAL.2005.10.005zbMATH Open1107.68090OpenAlexW1977189131WikidataQ56228326 ScholiaQ56228326MaRDI QIDQ865639FDOQ865639

Authors: Stuart Allen, R. Eaton, L. Lorigo, E. Moran, Mark Bickford, Robert Constable, Christoph Kreitz 

Publication date: 20 February 2007

Published in: Journal of Applied Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.jal.2005.10.005

Recommendations

• scientific article; zbMATH DE number 4053566
• scientific article; zbMATH DE number 1070622
• scientific article; zbMATH DE number 1301854
• scientific article; zbMATH DE number 3986665
• scientific article; zbMATH DE number 1614694

zbMATH Keywords

program extractiontacticscomputational type theorydependent intersection typesformal digital librarieslogic of eventspolymorphic subtypingproofs as programsunion typesMartin-Löf type theory

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Cites Work

• Title not available (Why is that?)
• Title not available (Why is that?)
• Edinburgh LCF. A mechanized logic of computation
• Title not available (Why is that?)
• Title not available (Why is that?)
• Emergence of Scaling in Random Networks
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Combinatory logic. With two sections by William Craig.
• Title not available (Why is that?)
• Data Types as Lattices
• Title not available (Why is that?)
• Title not available (Why is that?)
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Time, clocks, and the ordering of events in a distributed system
• Title not available (Why is that?)
• Constructivism in mathematics. An introduction. Volume II
• Title not available (Why is that?)
• Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
• Nuprl's class theory and its applications
• Intuitionistic completeness of first-order logic
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• The mutual exclusion problem
• Theorem proving in higher order logics. 16th international conference, TPHOLs 2003, Rome, Italy, September 8--12, 2003. Proceedings
• Title not available (Why is that?)
• Title not available (Why is that?)
• Constructive mathematics and computer programming
• An introduction to the PL/CV2 programming logic
• Writing programs that construct proofs
• Mathematical knowledge management in HELM
• A uniform procedure for converting matrix proofs into sequent-style systems
• Title not available (Why is that?)
• Toward sharing libraries of mathematics between theorem provers
• The Type Theory of PL/CV3
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Building reliable, high-performance networks with the Nuprl proof development system
• Exploring abstract algebra in constructive type theory
• Hybrid interactive theorem proving using nuprl and HOL
• Mathematical Knowledge Management
• Foundations for the implementation of higher-order subtyping

Cited In (23)

• Intuitionistic completeness of first-order logic
• ν-Types for Effects and Freshness Analysis
• Title not available (Why is that?)
• Manifest Fields and Module Mechanisms in Intensional Type Theory
• Formally computing with the non-computable
• Exercising Nuprl’s Open-Endedness
• A language with type-dependent equality
• \(\text{TT}^\Box_{\mathcal{C}}\): a family of extensional type theories with effectful realizers of continuity
• The effects of effects on constructivism
• Intuitionistic Ancestral Logic as a Dependently Typed Abstract Programming Language
• Title not available (Why is that?)
• Building Mathematics-Based Software Systems to Advance Science and Create Knowledge
• Nuprl's class theory and its applications
• Title not available (Why is that?)
• Title not available (Why is that?)
• Nuprl
• Implementing Euclid's straightedge and compass constructions in type theory
• Tactics for hierarchical proof
• Validating Brouwer's continuity principle for numbers using named exceptions
• A thorough treatment of highly-efficient NTRU instantiations
• Cartesian cubical computational type theory: Constructive reasoning with paths and equalities
• Impredicative encodings of inductive-inductive data in Cedille
• Monotone recursive types and recursive data representations in Cedille

Uses Software

• Coq
• PVS
• MetaPRL
• Automath
• OMDoc
• LCF
• JProver
• MathWeb
• Horus

This page was built for publication: Innovations in computational type theory using Nuprl

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q865639)