Constructive mathematics and computer programming
From MaRDI portal
Publication:3343983
DOI10.1098/rsta.1984.0073zbMath0552.03040OpenAlexW2106718208MaRDI QIDQ3343983
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
programming languagesintuitionistic logicintuitionistic type theoryAutomathrelations between constructive mathematics and computer programming
Abstract data types; algebraic specification (68Q65) General topics in the theory of software (68N01) Metamathematics of constructive systems (03F50) Intuitionistic mathematics (03F55)
Related Items
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
