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 (only showing first 100 items - show all)
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 ⋮ 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
This page was built for publication:
