scientific article

Bengt Nordström, Jan Smith, Kent Petersson

Publication date: 17 September 1992

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

program extraction Martin-Löf type theory Curry-Howard isomorphism

Introductory exposition (textbooks, tutorial papers, etc.) pertaining to mathematical logic and foundations (03-01) Logic in computer science (03B70) Research exposition (monographs, survey articles) pertaining to computer science (68-02) General topics in the theory of software (68N01) Second- and higher-order arithmetic and fragments (03F35)

Related Items

Nominal lambda calculus: an internal language for FM-Cartesian closed categories, J-Calc: a typed lambda calculus for intuitionistic justification logic, Realizability interpretation of generalized inductive definitions, Inductive families, A characterisation of elementary fibrations, Supercompilation for Martin-Lof's type theory, The strength of some Martin-Löf type theories, Dependently typed array programs don't go wrong, A formal semantics for DAI language NUML, Meaning and computing: two approaches to computable propositions, Set theory for verification. II: Induction and recursion, Terminating general recursion, Innovations in computational type theory using Nuprl, Is ZF a hack? Comparing the complexity of some (formalist interpretations of) foundational systems for mathematics, Constructive characterizations of bar subsets, Constructive sets in computable sets, A type theoretic interpretation of constructive domain theory, Quotient completion for the foundation of constructive mathematics, ``Inference versus consequence revisited: inference, consequence, conditional, implication, Martin-Löf complexes, More dependent types for distributed arrays, Intuitionistic completeness of first-order logic, N. G. de Bruijn (1918--2012) and his road to Automath, the earliest proof checker, Meaning explanations at higher dimension, Typing correspondence assertions for communication protocols, A modal type theory for formalizing trusted communications, A functional framework for agent-based models of exchange, On the \(T_{1}\) axiom and other separation properties in constructive point-free and point-set topology, Induction-recursion and initial algebras., Inductively generated formal topologies., Coalgebras in functional programming and type theory, Do-it-yourself type theory, Domain interpretations of Martin-Löf's partial type theory, Relative properties of frame language, Constructive metrisability in point-free topology., Some points in formal topology., Keeping calm in the face of change. Towards optimisation of FRP by reasoning about change, Proof-relevance of families of setoids and identity in type theory, Composition of deductions within the propositions-as-types paradigm, Static semantics, types, and binding time analysis, A formalized general theory of syntax with bindings: extended version, An intuitionistic theory of types with assumptions of high-arity variables, New foundations for fixpoint computations: FIX-hyperdoctrines and the FIX-logic, The extended calculus of constructions (ECC) with inductive types, Constructions of categories of setoids from proof-irrelevant families, Constructive belief reports, Adjectival and adverbial modification: the view from modern type theories, Constructing type systems over an operational semantics, On systems of definitions, induction and recursion, Complexity of subclasses of the intuitionistic propositional calculus, Remarks on Martin-Löf's partial type theory, On specifications, subset types and interpretation of proposition in type theory, Type-theoretic interpretation of iterated, strictly positive inductive definitions, The identity type weak factorisation system, Consistency of the intensional level of the minimalist foundation with Church's thesis and axiom of choice, Revisiting the categorical interpretation of dependent type theory, A dependent type theory with abstractable names, A constructive type-theoretical formalism for the interpretation of subatomically sensitive natural language constructions, Monads in double categories, Unifying exact completions, Curry-Howard for incomplete first-order logic derivations using one-and-a-half level terms, Preface to the special volume, External and internal syntax of the \(\lambda \)-calculus, Transitivity in coercive subtyping, A computer-verified monadic functional implementation of the integral, The simplicial model of univalent foundations (after Voevodsky), The justification of identity elimination in Martin-Löf's type theory, Proof, meaning and paradox: some remarks, N. G. de Bruijn's contribution to the formalization of mathematics, Isomorphism is equality, Verifying programs in the calculus of inductive constructions, On the strength of dependent products in the type theory of Martin-Löf, From constructivism to computer science, A minimalist two-level foundation for constructive mathematics, Harmony and autonomy in classical logic, Order-sorted inductive types, Mechanized metatheory revisited, Proof assistants: history, ideas and future, The universal exponentiable arrow, Proof-search in type-theoretic languages: An introduction, Predicativity and constructive mathematics, A categorical reading of the numerical existence property in constructive foundations, Well-ordering proofs for Martin-Löf type theory, Inaccessibility in constructive set theory and type theory, Five observations concerning the intended meaning of the intuitionistic logical constants, Formalizing constructive projective geometry in Agda, \(\pi\)-calculus in (Co)inductive-type theory, A Boolean model of ultrafilters, CASL: the Common Algebraic Specification Language., A cartesian closed category in Martin-Löf's intuitionistic type theory, On the formalization of the modal \(\mu\)-calculus in the calculus of inductive constructions, Propositions and specifications of programs in Martin-Löf's type theory, On the compatibility between the minimalist foundation and constructive set theory, From the universality of mathematical truth to the interoperability of proof systems, Defining concurrent processes constructively, Normalising the associative law: An experiment with Martin-Löf's type theory, Set theory for verification. I: From foundations to functions, Synthesis of ML programs in the system Coq, \(QPC_ 2\): A constructive calculus with parameterized specifications, Toward formal development of programs from algebraic specifications: Parameterisation revisited, From type theory to setoids and back, Negative predication and distinctness, Propositional forms of judgemental interpretations, The metatheory of UTT, The placeholder view of assumptions and the Curry-Howard correspondence, A Comparison of Type Theory with Set Theory, Formalising Mathematics in Simple Type Theory, Infinite objects in type theory, Elimination of extensionality in Martin-Löf type theory, Programming with streams in Coq a case study: The Sieve of Eratosthenes, The Alf proof editor and its proof engine, The expressive power of Structural Operational Semantics with explicit assumptions, Type theory and the informal language of mathematics, A short and flexible proof of strong normalization for the calculus of constructions, Primitive recursive functional with dependent types, The compatibility of the minimalist foundation with homotopy type theory, A general framework for the semantics of type theory, UNDER LOCK AND KEY: A PROOF SYSTEM FOR A MULTIMODAL LOGIC, Unnamed Item, Semantics of constructions. I: The traditional approach, A light-weight integration of automated and interactive theorem proving, Semantics of constructions. II: The initial algebraic approach, Coercion completion and conservativity in coercive subtyping, Least and greatest fixed points in intuitionistic natural deduction, Primitive recursion for higher-order abstract syntax, The practice of logical frameworks, Formal topologies on the set of first-order formulae, Linear Dependent Type Theory for Quantum Programming Languages, Applications of type theory, Homotopical patch theory, Combining Model Checking and Data-Flow Analysis, Cubical methods in homotopy type theory and univalent foundations, Certifying Supercompilation for Martin-Löf’s Type Theory, Data Types with Symmetries and Polynomial Functors over Groupoids, Categorical reconstruction of a reduction free normalization proof, Hom weak ω-categories of a weak ω-category, Inductive and Coinductive Topological Generation with Church's thesis and the Axiom of Choice, A Minimalist Foundation at Work, A Brief Overview of Agda – A Functional Language with Dependent Types, Translating a Dependently-Typed Logic to First-Order Logic, A higher-order calculus and theory abstraction, Program specification and data refinement in type theory, A structural investigation on formal topology: coreflection of formal covers and exponentiability, Algorithmic Theories of Problems. A Constructive and a Non-Constructive Approach, Characteristics of de Bruijn’s early proof checker Automath, The Friedman‐Translation for Martin‐Löf's Type Theory, Type theory as a foundation for computer science, Some normalization properties of martin-löf's type theory, and applications, Singleton, union and intersection types for program extraction, Intuitionistic Ancestral Logic as a Dependently Typed Abstract Programming Language, Finiteness in a Minimalist Foundation, Constructing a small category of setoids, Realist Consequence, Epistemic Inference, Computational Correctness, Identity types and weak factorization systems in Cauchy complete categories, Implementing Variable Vectors in a CCG Parser, Unnamed Item, Identity and intensionality in univalent foundations and philosophy, The placeholder view of assumptions and the Curry-Howard correspondence (extended abstract), An Intuitionistic Version of Cantor's Theorem, Structural subtyping for inductive types with functorial equality rules, Constructive Sheaf Semantics, On Choice Rules in Dependent Type Theory, Decidability in Intuitionistic Type Theory is Functionally Decidable, A Type of Partial Recursive Functions, Type theoretic semantics for SemNet, EXACT COMPLETION AND CONSTRUCTIVE THEORIES OF SETS, Polynomial functors and polynomial monads, Homotopy-Theoretic Models of Type Theory, Homotopy type-theoretic interpretations of constructive set theories, Reflection of formal tactics in a deductive reflection framework, A two-level approach towards lean proof-checking, A constructive proof of the Heine-Borel covering theorem for formal reals, Conservativity of equality reflection over intensional type theory, Optimized encodings of fragments of type theory in first order logic, A PREDICATIVE VARIANT OF HYLAND’S EFFECTIVE TOPOS, Interpreting descriptions in intensional type theory, Structural recursion with locally scoped names, Tychonoff's theorem in the framework of formal topologies, Roles, stacks, histories: A triple for Hoare, Unnamed Item, Typing Correspondence Assertions for Communication Protocols, 2-Dimensional Directed Type Theory, Compositional Coinduction with Sized Types, Setoids and universes, Partiality and recursion in interactive theorem provers – an overview, The Functional Interpretation of Direct Computations, Intuitionistic categorial grammar, Homotopy theoretic models of identity types, Introduction to Type Theory, Dependent Types at Work, Unnamed Item, Interfaces as functors, programs as coalgebras -- a final coalgebra theorem in intensional type theory, XI Latin American Symposium on Mathematical Logic, Unnamed Item, Declarative Foreign Function Binding Through Generic Programming, Multisets in type theory, A UNIVERSE OF STRICTLY POSITIVE FAMILIES, Proof Theory of Constructive Systems: Inductive Types and Univalence, Dual Calculus with Inductive and Coinductive Types, A Modular Type-Checking Algorithm for Type Theory with Singleton Types and Proof Irrelevance, Manifest Fields and Module Mechanisms in Intensional Type Theory, Big-step normalisation, Classical mathematics for a constructive world, Two-dimensional models of type theory, W-types in setoids, ETA-RULES IN MARTIN-LÖF TYPE THEORY, Joyal's arithmetic universes via type theory, List Objects with Algebraic Structure, Containers: Constructing strictly positive types, Natural Deduction for Equality: The Missing Entity, Book review of: B. Steffen et al., Mathematical foundations of advanced informatics. Volume 1. Inductive approaches, Encoding FIX in Object Calculi, Type Theory and Homotopy, Machine Translation and Type Theory, Coalgebras as Types Determined by Their Elimination Rules, Pretopologies and a uniform presentation of sup-lattices, quantales and frames, On the collection of points of a formal space, Programming interfaces and basic topology, Formal Zariski topology: Positivity and points, Indexed induction-recursion, Lightweight Static Capabilities, Normalization by Evaluation for Martin-Löf Type Theory with One Universe, Extensional equality preservation and verified generic programming, A Logical Framework with Explicit Conversions, Meta-programming With Built-in Type Equality, REFLECTIONS ON MATHEMATICAL ECONOMICS IN THE ALGORITHMIC MODE