scientific article

Publication date: 1982

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

programming languages intuitionistic logic intuitionistic type theory Automath relations 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

The origins of structural operational semantics, From type theory to setoids and back, A characterisation of elementary fibrations, Applications of type theory, Towards a directed homotopy type theory, Insight in discrete geometry and computational content of a discrete model of the continuum, Cubical methods in homotopy type theory and univalent foundations, A small complete category, Middle-out reasoning for synthesis and induction, Homotopy type theory and Voevodsky’s univalent foundations, 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, Type theory as a foundation for computer science, Some normalization properties of martin-löf's type theory, and applications, A generic algebra for data collections based on constructive logic, Intuitionistic completeness of first-order logic, Intuitionistic Ancestral Logic as a Dependently Typed Abstract Programming Language, Finitary type theories with and without contexts, A Survey of the Proof-Theoretic Foundations of Logic Programming, Univalent Foundations and the UniMath Library, A Comparison of Type Theory with Set Theory, Martin-Löf identity types in C-systems, POPLMark reloaded: Mechanizing proofs by logical relations, Using formal methods with SysML in aerospace design and engineering, Induction-recursion and initial algebras., Coalgebras in functional programming and type theory, Constructive system for automatic program synthesis, Some points in formal topology., Unnamed Item, Between constructive mathematics and PROLOG, Partial inductive definitions, Static semantics, types, and binding time analysis, From Mathesis Universalis to Provability, Computability, and Constructivity, Process calculus based upon evaluation to committed form, A higher-order interpretation of deductive tableau, A computer-verified monadic functional implementation of the integral, Connectionist computations of intuitionistic reasoning, A type-theoretic approach to program development, An introduction to univalent foundations for mathematicians, On the proof theory of Coquand's calculus of constructions, The justification of identity elimination in Martin-Löf's type theory, A Classical Realizability Model for a Semantical Value Restriction, Constructive Mathematics and Functional Programming (Abstract), A First Look into a Formal and Constructive Approach for Discrete Geometry Using Nonstandard Analysis, THE CONCEPTHORSEIS A CONCEPT, Exploring abstract algebra in constructive type theory, A meaning explanation for HoTT, Applause: An implementation of the Collins-Michalski theory of plausible reasoning, An adequacy theorem for dependent type theory, Building Mathematics-Based Software Systems to Advance Science and Create Knowledge, W-types in setoids, Unnamed Item, A Proposal for Broad Spectrum Proof Certificates, From signatures to monads in \textsf{UniMath}, ETA-RULES IN MARTIN-LÖF TYPE THEORY, Proof-search in type-theoretic languages: An introduction, Predicativity and constructive mathematics, Predicative functionals and an interpretation of \({\widehat{\text{ID}}_{<\omega}}\), Natural Deduction for Equality: The Missing Entity, Truth and Proof in Intuitionism, Program Testing and the Meaning Explanations of Intuitionistic Type Theory, Constructive algebraic integration theory, Categories with Families: Unityped, Simply Typed, and Dependently Typed, Theory of Constructive Semigroups with Apartness – Foundations, Development and Practice, A type- and scope-safe universe of syntaxes with binding: their semantics and proofs, IMPS: An interactive mathematical proof system, Formally computing with the non-computable, The practice of logical frameworks