Constructive mathematics and computer programming

DOI10.1098/RSTA.1984.0073MaRDI QIDQ3343983zbMATH OpenOpenAlexFDO

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)

• Functorial polymorphism
• About primitive recursive algorithms
• Do-it-yourself type theory
• Constructive Mathematics in Theory and Programming Practice
• The interpretation of intuitionistic type theory in locally Cartesian closed categories -- an intuitionistic perspective
• Algebra of constructions. I. The word problem for partial algebras
• Domain interpretations of Martin-Löf's partial type theory
• scientific article; zbMATH DE number 53194 (Why is no real title available?)
• 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
• Towards a computation system based on set theory
• Foundational aspects of multiscale digitization
• Normalization by Evaluation for Martin-Löf Type Theory with One Universe
• Type checking with universes
• A bridge between constructive logic and computer programming
• The Girard-Reynolds isomorphism
• Computational foundations of basic recursive function theory
• Realizability interpretation of generalized inductive definitions
• Analogical program derivation based on type theory
• Innovations in computational type theory using Nuprl
• From LCF to Isabelle/HOL
• Proof-theoretical analysis: Weak systems of functions and classes
• HasCasl: integrated higher-order specification and program development
• One step is enough
• The calculus of constructions
• Program development in constructive type theory
• An intuitionistic theory of types with assumptions of high-arity variables
• Computational logic: its origins and applications
• Possible forms of evaluation or reduction in Martin-Löf type theory
• scientific article; zbMATH DE number 7225974 (Why is no real title available?)
• A constructive approach to state description semantics
• Cartesian cubical computational type theory: Constructive reasoning with paths and equalities
• 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

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)