Innovations in computational type theory using Nuprl
From MaRDI portal
Publication:865639
DOI10.1016/j.jal.2005.10.005zbMath1107.68090OpenAlexW1977189131WikidataQ56228326 ScholiaQ56228326MaRDI QIDQ865639
L. Lorigo, R. Eaton, E. Moran, S. F. Allen, Christoph Kreitz, Mark Bickford, Robert L. Constable
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
program extractionMartin-Löf type theorytacticscomputational type theorydependent intersection typesformal digital librarieslogic of eventspolymorphic subtypingproofs as programsunion types
Related Items
A language with type-dependent equality, The effects of effects on constructivism, Implementing Euclid's straightedge and compass constructions in type theory, Monotone recursive types and recursive data representations in Cedille, Intuitionistic completeness of first-order logic, Intuitionistic Ancestral Logic as a Dependently Typed Abstract Programming Language, Tactics for hierarchical proof, Unnamed Item, Validating Brouwer's continuity principle for numbers using named exceptions, Cartesian cubical computational type theory: Constructive reasoning with paths and equalities, Exercising Nuprl’s Open-Endedness, Nuprl, Manifest Fields and Module Mechanisms in Intensional Type Theory, Building Mathematics-Based Software Systems to Advance Science and Create Knowledge, Formally computing with the non-computable
Uses Software
Cites Work
- Intuitionistic completeness of first-order logic
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- Combinatory logic. With two sections by William Craig.
- An introduction to the PL/CV2 programming logic
- Constructivism in mathematics. An introduction. Volume II
- Theorem proving in higher order logics. 16th international conference, TPHOLs 2003, Rome, Italy, September 8--12, 2003. Proceedings
- Edinburgh LCF. A mechanized logic of computation
- Mathematical knowledge management in HELM
- Writing programs that construct proofs
- A uniform procedure for converting matrix proofs into sequent-style systems
- Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
- Emergence of Scaling in Random Networks
- Constructive mathematics and computer programming
- The Type Theory of PL/CV3
- Data Types as Lattices
- Time, clocks, and the ordering of events in a distributed system
- 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
- The mutual exclusion problem
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
