Constructive mathematics and computer programming

DOI10.1098/RSTA.1984.0073zbMath0552.03040OpenAlexW2106718208MaRDI QIDQ3343983

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

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

Related Items (45)

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

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