Constructive mathematics and computer programming

DOI10.1098/RSTA.1984.0073zbMATH Open0552.03040OpenAlexW2106718208MaRDI QIDQ3343983FDOQ3343983

Authors: Per Martin-Löf 

Publication date: 1984

Published in: Philosophical Transactions of the Royal Society of London. Series A, Mathematical and Physical Sciences (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1098/rsta.1984.0073

zbMATH Keywords

programming languagesintuitionistic logicintuitionistic type theoryAutomathrelations between constructive mathematics and computer programming

Mathematics Subject Classification ID

General topics in the theory of software (68N01) Metamathematics of constructive systems (03F50) Abstract data types; algebraic specification (68Q65) Intuitionistic mathematics (03F55)

Cited In (49)

• About primitive recursive algorithms
• Constructive Mathematics in Theory and Programming Practice
• The interpretation of intuitionistic type theory in locally Cartesian closed categories -- an intuitionistic perspective
• Do-it-yourself type theory
• Algebra of constructions. I. The word problem for partial algebras
• Domain interpretations of Martin-Löf's partial type theory
• Title not available (Why is that?)
• Nonconstructive computational mathematics
• Representing scope in intuitionistic deductions
• Process calculus based upon evaluation to committed form
• Constructing type systems over an operational semantics
• From constructivism to computer science
• Axiomatizing geometric constructions
• Generalized algebraic theories and contextual categories
• Indexed induction-recursion
• The axioms of constructive geometry
• The Girard-Reynolds isomorphism (second edition)
• Formal methods in the philosophy of science
• Extraction and verification of programs by analysis of formal proofs
• System \(T\), call-by-value and the minimum problem
• Extended bar induction in applicative theories
• Normalization by Evaluation for Martin-Löf Type Theory with One Universe
• Towards a computation system based on set theory
• Foundational aspects of multiscale digitization
• Type checking with universes
• A bridge between constructive logic and computer programming
• The Girard-Reynolds isomorphism
• Analogical program derivation based on type theory
• Computational foundations of basic recursive function theory
• Realizability interpretation of generalized inductive definitions
• From LCF to Isabelle/HOL
• Innovations in computational type theory using Nuprl
• Proof-theoretical analysis: Weak systems of functions and classes
• HasCasl: integrated higher-order specification and program development
• One step is enough
• Computational logic: its origins and applications
• The calculus of constructions
• Program development in constructive type theory
• An intuitionistic theory of types with assumptions of high-arity variables
• Possible forms of evaluation or reduction in Martin-Löf type theory
• Title not available (Why is that?)
• Cartesian cubical computational type theory: Constructive reasoning with paths and equalities
• A constructive approach to state description semantics
• On the syntax of Martin-Löf's type theories
• Well-ordering proofs for Martin-Löf type theory
• Representing inductively defined sets by wellorderings in Martin-Löf's type theory
• Inverse semigroups with apartness
• Constructing recursion operators in intuitionistic type theory
• Functorial polymorphism

This page was built for publication: Constructive mathematics and computer programming

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