scientific article; zbMATH DE number 3521950
From MaRDI portal
Publication:4099613
zbMath0334.02016MaRDI QIDQ4099613
Publication date: 1975
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Related Items
Normalization by evaluation and algebraic effects, Category theory, logic and formal linguistics: some connections, old and new, Unnamed Item, Finitary higher inductive types in the groupoid model, Inductive families, A characterisation of elementary fibrations, Apartness spaces and uniform neighbourhood structures, Representations and the foundations of mathematics, Generic Literals, Cubical methods in homotopy type theory and univalent foundations, Categorical reconstruction of a reduction free normalization proof, On the syntax of Martin-Löf's type theories, A constructive valuation semantics for classical logic, A higher-order calculus and theory abstraction, Pebble, a kernel language for modules and abstract data types, I Got Plenty o’ Nuttin’, The calculus of constructions, Computational logic: its origins and applications, Error and Predicativity, Innovations in computational type theory using Nuprl, Algorithmic Theories of Problems. A Constructive and a Non-Constructive Approach, On Church's formal theory of functions and functionals. The \(\lambda\)- calculus: Connections to higher type recursion theory, proof theory, category theory, Generalization from partial parametrization in higher-order type theory, Size-based termination of higher-order rewriting, Martin-Löf complexes, Type theory as a foundation for computer science, A scalable module system, Intuitionistic completeness of first-order logic, Unnamed Item, Observability in the univalent universe, Meaning explanations at higher dimension, To be or not to be constructive, that is not the question, Canonicity and normalization for dependent type theory, Inverse linking, possessive weak definites and Haddock descriptions: a unified dependent type account, On the Cognitive and Theoretical Foundations of Big Data Science and Engineering, Meta-circular interpreter for a strongly typed language, Identity and intensionality in univalent foundations and philosophy, Induction-recursion and initial algebras., Leibniz equality is isomorphic to Martin-Löf identity, parametrically, Coalgebras in functional programming and type theory, Proof-theoretical analysis: Weak systems of functions and classes, Constructive system for automatic program synthesis, Constructivist and structuralist foundations: Bishop's and Lawvere's theories of sets, Formal neighbourhoods, combinatory Böhm trees, and untyped normalization by evaluation, Representing model theory in a type-theoretical logical framework, Unnamed Item, Type checking with universes, Proof normalization with nonstandard objects, Composition of deductions within the propositions-as-types paradigm, Constructing a universe for the setoid model, From Mathesis Universalis to Provability, Computability, and Constructivity, An intuitionistic theory of types with assumptions of high-arity variables, Map theory, Adjectival and adverbial modification: the view from modern type theories, Constructing type systems over an operational semantics, Coquand's calculus of constructions: A mathematical foundation for a proof development system, Type-theoretic interpretation of iterated, strictly positive inductive definitions, Natural language inference in Coq, Independence results around constructive ZF, Cubical Type Theory: a constructive interpretation of the univalence axiom, Intuitionistic categorial grammar, Characterizing the interpretation of set theory in Martin-Löf type theory, Unnamed Item, An introduction to univalent foundations for mathematicians, Unnamed Item, Univalence as a principle of logic, Combinatorial topology and constructive mathematics, The seeming interdependence between the concepts of valid inference and proof, The justification of identity elimination in Martin-Löf's type theory, Filter quotients and non-presentable \((\infty,1)\)-toposes, Isomorphism is equality, Reverse formalism 16, Equational type logic, From constructivism to computer science, Normalization by Evaluation for Typed Weak lambda-Reduction, Towards a computation system based on set theory, Guarded cubical type theory, Unnamed Item, Proof-search in type-theoretic languages: An introduction, Variations on inductive-recursive definitions, Models of Type Theory Based on Moore Paths, Predicativity and constructive mathematics, A categorical reading of the numerical existence property in constructive foundations, Constructive mathematics: a foundation for computable analysis, Continuity and Lipschitz constants for projections, Containers: Constructing strictly positive types, Reflections on reflections in explicit mathematics, Predicative functionals and an interpretation of \({\widehat{\text{ID}}_{<\omega}}\), Well-ordering proofs for Martin-Löf type theory, Inaccessibility in constructive set theory and type theory, Programs as proofs: A synopsis, Realizability and intuitionistic logic, A proof description language and its reduction system, Natural models of homotopy type theory, Propositions and specifications of programs in Martin-Löf's type theory, Cubical Agda: A dependently typed programming language with univalence and higher inductive types, Algebras of complemented subsets, The Equivalence of Complete Reductions, Constructive mathematics, Church's thesis, and free choice sequences, A selected bibliography on constructive mathematics, intuitionistic type theory and higher order deduction, THE AXIOM OF CHOICE IS FALSE INTUITIONISTICALLY (IN MOST CONTEXTS), Propositional forms of judgemental interpretations, Normalization by evaluation for modal dependent type theory, Formalising Mathematics in Simple Type Theory, Primitive recursive functional with dependent types, Morphism equality in theory graphs, Strange new universes: Proof assistants and synthetic foundations, Reduction Free Normalisation for a proof irrelevant type of propositions, Martin-Löf identity types in C-systems, On the ∞$\infty$‐topos semantics of homotopy type theory, Spiritus asper versus lambda: on the nature of functional abstraction, Unnamed Item, What should a generic object be?, Denotational semantics for guarded dependent type theory, The Functional Interpretation of Direct Computations, Inductive-data-type systems, On the proof theory of Coquand's calculus of constructions, Why Sets?, COMPUTABILITY THEORY, NONSTANDARD ANALYSIS, AND THEIR CONNECTIONS, Predicativity and Feferman, ETA-RULES IN MARTIN-LÖF TYPE THEORY, Natural Deduction for Equality: The Missing Entity, Unnamed Item, Truth and Proof in Intuitionism, Primitive Recursive Arithmetic and Its Role in the Foundations of Arithmetic: Historical and Philosophical Reflections, Type Theory and Homotopy, Program Testing and the Meaning Explanations of Intuitionistic Type Theory
