scientific article; zbMATH DE number 3859117
From MaRDI portal
Publication:3328540
zbMATH Open0541.03034MaRDI QIDQ3328540FDOQ3328540
Authors: Per Martin-Löf 
Publication date: 1982
Title of this publication is not available (Why is that?)
Recommendations
programming languagesintuitionistic logicintuitionistic type theoryAutomathrelations between constructive mathematics and computer programming
General topics in the theory of software (68N01) Metamathematics of constructive systems (03F50) Abstract data types; algebraic specification (68Q65) Intuitionistic mathematics (03F55)
Cited In (81)
- Intuitionistic completeness of first-order logic
- A type-theoretic approach to program development
- Martin-Löf identity types in C-systems
- From signatures to monads in \textsf{UniMath}
- A characterisation of elementary fibrations
- An adequacy theorem for dependent type theory
- Partial inductive definitions
- Insight in discrete geometry and computational content of a discrete model of the continuum
- Programming by example and proving by example using higher-order unification
- On the relationship between foundations of programming and mathematics
- Constructive Mathematics in Theory and Programming Practice
- A selected bibliography on constructive mathematics, intuitionistic type theory and higher order deduction
- Formally computing with the non-computable
- Exploring abstract algebra in constructive type theory
- The origins of structural operational semantics
- Induction-recursion and initial algebras.
- A proposal for broad spectrum proof certificates
- Natural Deduction for Equality: The Missing Entity
- Program Testing and the Meaning Explanations of Intuitionistic Type Theory
- Constructive algebraic integration theory
- Nonconstructive computational mathematics
- Process calculus based upon evaluation to committed form
- Connectionist computations of intuitionistic reasoning
- Using formal methods with SysML in aerospace design and engineering
- Towards a directed homotopy type theory
- Intuitionistic Ancestral Logic as a Dependently Typed Abstract Programming Language
- POPLMark reloaded: Mechanizing proofs by logical relations
- Some points in formal topology.
- From type theory to setoids and back
- Title not available (Why is that?)
- Predicative functionals and an interpretation of \({\widehat{\text{ID}}_{<\omega}}\)
- A Comparison of Type Theory with Set Theory
- Homotopy type theory and Voevodsky’s univalent foundations
- A Classical Realizability Model for a Semantical Value Restriction
- The justification of identity elimination in Martin-Löf's type theory
- Building Mathematics-Based Software Systems to Advance Science and Create Knowledge
- Applications of type theory
- Applause: An implementation of the Collins-Michalski theory of plausible reasoning
- Between constructive mathematics and PROLOG
- Title not available (Why is that?)
- Finitary type theories with and without contexts
- A meaning explanation for HoTT
- Static semantics, types, and binding time analysis
- Truth and Proof in Intuitionism
- Coalgebras in functional programming and type theory
- A small complete category
- Constructive system for automatic program synthesis
- From Mathesis Universalis to Provability, Computability, and Constructivity
- On Church's formal theory of functions and functionals. The \(\lambda\)- calculus: Connections to higher type recursion theory, proof theory, category theory
- Turing-Completeness Totally Free
- IMPS: An interactive mathematical proof system
- A computer-verified monadic functional implementation of the integral
- Predicativity and constructive mathematics
- A higher-order interpretation of deductive tableau
- An introduction to univalent foundations for mathematicians
- Title not available (Why is that?)
- Proof-search in type-theoretic languages: An introduction
- A Survey of the Proof-Theoretic Foundations of Logic Programming
- The practice of logical frameworks
- Middle-out reasoning for synthesis and induction
- A type- and scope-safe universe of syntaxes with binding: their semantics and proofs
- A First Look into a Formal and Constructive Approach for Discrete Geometry Using Nonstandard Analysis
- On the proof theory of Coquand's calculus of constructions
- THE CONCEPTHORSEIS A CONCEPT
- A generic algebra for data collections based on constructive logic
- Some normalization properties of martin-löf's type theory, and applications
- A comparison of HOL and ALF formalizations of a categorical coherence theorem
- Importing mathematics from HOL into Nuprl
- ETA-RULES IN MARTIN-LÖF TYPE THEORY
- Theory of Constructive Semigroups with Apartness – Foundations, Development and Practice
- Topological quantum gates in homotopy type theory
- Title not available (Why is that?)
- Type theory as a foundation for computer science
- Title not available (Why is that?)
- Title not available (Why is that?)
- Categories with Families: Unityped, Simply Typed, and Dependently Typed
- Univalent Foundations and the UniMath Library
- W-types in setoids
- Cubical methods in homotopy type theory and univalent foundations
- Constructive Mathematics and Functional Programming (Abstract)
- RZ: a Tool for Bringing Constructive and Computable Mathematics Closer to Programming Practice
This page was built for publication:
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3328540)
