scientific article
From MaRDI portal
zbMath0571.03030MaRDI QIDQ3688389
Publication date: 1984
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations (03-02) Metamathematics of constructive systems (03F50) Intuitionistic mathematics (03F55)
Related Items
THE AXIOM OF CHOICE IS FALSE INTUITIONISTICALLY (IN MOST CONTEXTS), Type Theoretical Databases, The Urysohn Extension Theorem for Bishop Spaces, From type theory to setoids and back, Martin Hofmann’s contributions to type theory: Groupoids and univalence, On generalized algebraic theories and categories with families, Adding proof objects and inductive definition mechanisms to frege structures, A generic algebra for data collections based on constructive logic, Negative predication and distinctness, Extensional proofs in a propositional logic modulo isomorphisms, A user's friendly syntax to define recursive functions as typed λ-terms, Expressing computational complexity in constructive type theory, The placeholder view of assumptions and the Curry-Howard correspondence, Models of HoTT and the Constructive View of Theories, A Comparison of Type Theory with Set Theory, Elimination of extensionality in Martin-Löf type theory, A short and flexible proof of strong normalization for the calculus of constructions, Admissible ordering on monomials is well-founded: a constructive proof, Embedding \(\mathsf{HTLCG}\) into \(\mathsf{LCG}_\phi \), Generalising the fan theorem, The compatibility of the minimalist foundation with homotopy type theory, Strange new universes: Proof assistants and synthetic foundations, Cardinality reduction theorem for logics QHC and QH4, The formal verification of the ctm approach to forcing, Algebraic effects for extensible dynamic semantics, Spiritus asper versus lambda: on the nature of functional abstraction, Programming with ornaments, Interactive programming in Agda – Objects and graphical user interfaces, The essence of ornaments, The calculus of dependent lambda eliminations, Unnamed Item, Unnamed Item, An Intuitionistic Version of Cantor's Theorem, The Arrow-Hahn Construction in a Locally Compact Metric Space, Type Theory Unchained : Extending Agda with User-Defined Rewrite Rules, The Interpretation of Intuitionistic Type Theory in Locally Cartesian Closed Categories – an Intuitionistic Perspective, A type reduction from proof-conditional to dynamic semantics, Introduction to Type Theory, Dependent Types at Work, Unnamed Item, Unnamed Item, Unnamed Item, Type theories, toposes and constructive set theory: Predicative aspects of AST, Translating between Language and Logic: What Is Easy and What Is Difficult, Dialectic, the Dictum de Omni and Ecthesis, Prawitz, Proofs, and Meaning, Constructibility and Geometry, Cartesian cubical computational type theory: Constructive reasoning with paths and equalities, Computable analysis with applications to dynamic systems, Every countably presented formal topology is spatial, classically, W-types in setoids, Unnamed Item, ETA-RULES IN MARTIN-LÖF TYPE THEORY, Variations on inductive-recursive definitions, Proof-Theoretic Semantics and Feasibility, Generalized Elimination Inferences, Higher-Level Rules, and the Implications-as-Rules Interpretation of the Sequent Calculus, Wittgenstein’s Diagonal Argument: A Variation on Cantor and Turing, Truth and Proof in Intuitionism, Type Theory and Homotopy, Program Testing and the Meaning Explanations of Intuitionistic Type Theory, Machine Translation and Type Theory, Constructive Zermelo-Fraenkel Set Theory, Power Set, and the Calculus of Constructions, Coalgebras as Types Determined by Their Elimination Rules, Normalization by Evaluation for Martin-Löf Type Theory with One Universe, Two decades of automatic amortized resource analysis, A rewriting coherence theorem with applications in homotopy type theory, Interpretation of constructive multi-typed theory in the theory of arithmetical truth, Proofs, grounds and empty functions: epistemic compulsion in Prawitz's semantics, J-Calc: a typed lambda calculus for intuitionistic justification logic, Category theory, logic and formal linguistics: some connections, old and new, Selectional restrictions, types and categories, Finitary higher inductive types in the groupoid model, Inductive families, A characterisation of elementary fibrations, A constructive manifestation of the Kleene-Kreisel continuous functionals, Apartness spaces and uniform neighbourhood structures, The strength of some Martin-Löf type theories, Calculi of epistemic grounding based on Prawitz's theory of grounds, Constructive domain theory as a branch of intuitionistic pointfree topology, A note on ``A simplified account of polymorphic references, On completeness and cocompleteness in and around small categories, On the syntax of Martin-Löf's type theories, Meaning and computing: two approaches to computable propositions, Voting theory in the Lean theorem prover, A sheaf-theoretic foundation for nonstandard analysis, Justification logic and type theory as formalizations of intuitionistic propositional logic, The linear abstract machine, Levels of truth, The calculus of constructions, Innovations in computational type theory using Nuprl, Constructive characterizations of bar subsets, On Church's formal theory of functions and functionals. The \(\lambda\)- calculus: Connections to higher type recursion theory, proof theory, category theory, The epistemic significance of valid inference, ``Inference versus consequence revisited: inference, consequence, conditional, implication, Exact approximations to Stone-Čech compactification, The basic Zariski topology, A general adequacy result for a linear functional language, Representing inductively defined sets by wellorderings in Martin-Löf's type theory, Non-deterministic inductive definitions, Arithmetical conservation results, Figures of dialogue: a view from ludics, Dialogue structure and logical expressivism, From the knowability paradox to the existence of proofs, Setting the facts straight, In defense of logical universalism: taking issue with Jean van Heijenoort, A modal type theory for formalizing trusted communications, Characterization of quantum states in predicative logic, Induction-recursion and initial algebras., Identity and sortals (and Caesar), Coalgebras in functional programming and type theory, Homotopical inverse diagrams in categories with attributes, Do-it-yourself type theory, Univalent foundations as structuralist foundations, On a machine-checked proof for fraction arithmetic over a GCD domain, Dual and axiomatic systems for constructive S4, a formally verified equivalence, Constructive metrisability in point-free topology., Between constructive mathematics and PROLOG, Type checking with universes, Mathematical logic: proof theory, constructive mathematics. Abstracts from the workshop held November 5--11, 2017, Static semantics, types, and binding time analysis, Free choice sequences: a temporal interpretation compatible with acceptance of classical mathematics, The seven virtues of simple type theory, Recursive programming with proofs, Alpha-structural induction and recursion for the lambda calculus in constructive type theory, The Zariski spectrum as a formal geometry, Constructive belief reports, Adjectival and adverbial modification: the view from modern type theories, Incorporating quotation and evaluation into Church's type theory, Aspects of predicative algebraic set theory. I: Exact completion, On specifications, subset types and interpretation of proposition in type theory, Type-theoretic interpretation of iterated, strictly positive inductive definitions, Polynomial-time Martin-Löf type theory, Consistency of the intensional level of the minimalist foundation with Church's thesis and axiom of choice, Objects: a study in Kantian formal epistemology, A dependent type theory with abstractable names, Formalisation in constructive type theory of Stoughton's substitution for the lambda calculus, Comprehension categories and the semantics of type dependency, The undecidability of pattern matching in calculi where primitive recursive functions are representable, The problem of the formalization of constructive topology, Independence results around constructive ZF, Computer theorem proving in mathematics, Transitivity in coercive subtyping, Functorial data migration, Exception tracking in an open world, N. G. de Bruijn's contribution to the formalization of mathematics, A note on inconsistencies caused by fixpoints in a cartesian closed category, A meaning explanation for HoTT, Verifying programs in the calculus of inductive constructions, A unary representation result for system \(T\), A note on complexity measures for inductive classes in constructive type theory, System \(T\), call-by-value and the minimum problem, A minimalist two-level foundation for constructive mathematics, Morse set theory as a foundation for constructive mathematics, Game of grounds, Predicativity and constructive mathematics, A categorical reading of the numerical existence property in constructive foundations, 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, IDL-PMCFG, a grammar formalism for describing free word order languages, A cartesian closed category in Martin-Löf's intuitionistic type theory, On the compatibility between the minimalist foundation and constructive set theory, Synthesis of ML programs in the system Coq, \(QPC_ 2\): A constructive calculus with parameterized specifications, A selected bibliography on constructive mathematics, intuitionistic type theory and higher order deduction, Denotational semantics for languages of epistemic grounding based on Prawitz's theory of grounds, Formal metatheory of the lambda calculus using Stoughton's substitution, Formalization of Habanero phasers using Coq, Spatiality and classical logic, General proof theory: introduction, The fundamental problem of general proof theory, Are there enough injective sets?, Cubical methods in homotopy type theory and univalent foundations, Certifying Supercompilation for Martin-Löf’s Type Theory, Axiomatic Thinking, Identity of Proofs and the Quest for an Intensional Proof-Theoretic Semantics, Data Types with Symmetries and Polynomial Functors over Groupoids, From realizability to induction via dependent intersection, A Minimalist Foundation at Work, A Brief Overview of Agda – A Functional Language with Dependent Types, Introducing data types in intuitionistic type theory, A higher-order calculus and theory abstraction, Algorithmic Theories of Problems. A Constructive and a Non-Constructive Approach, Homotopy type theory and Voevodsky’s univalent foundations, Intuitionistic Ancestral Logic as a Dependently Typed Abstract Programming Language, Finiteness in a Minimalist Foundation, Universal properties of bicategories of polynomials, Representing types as neural events, Inverse linking, possessive weak definites and Haddock descriptions: a unified dependent type account, Variable handling and compositionality: comparing DRT and DTS, The Interpretation Lifting Theorem for C-Systems, Implementing Variable Vectors in a CCG Parser, Unnamed Item, The intensional side of algebraic-topological representation theorems, Proof-theoretic harmony: towards an intensional account, Identity and intensionality in univalent foundations and philosophy, The placeholder view of assumptions and the Curry-Howard correspondence (extended abstract), Infinity and verifiability in Carnap's inductive logic, Intuitionistic fixed point logic, On Choice Rules in Dependent Type Theory, Decidability in Intuitionistic Type Theory is Functionally Decidable, The Axiom of Choice as Interaction Brief Remarks on the Principle of Dependent Choices in a Dialogical Setting, Composition of deductions within the propositions-as-types paradigm, The assertion-candidate and the meaning of mood, Constructing a universe for the setoid model, Graded modal dependent type theory, Mathesis Universalis and Homotopy Type Theory, On the Constructive and Computational Content of Abstract Mathematics, Dialogues, Reasons and Endorsement, Validating Brouwer's continuity principle for numbers using named exceptions, The Biequivalence of Locally Cartesian Closed Categories and Martin-Löf Type Theories, A constructive proof of the Heine-Borel covering theorem for formal reals, Conservativity of equality reflection over intensional type theory, Context-relative syntactic categories and the formalization of mathematical text, Unnamed Item, Formalizing Type Operations Using the “Image” Type Constructor, Axiomatizing geometric constructions, Natural language inference in Coq, Setoids and universes, Constructive completions of ordered sets, groups and fields, Quotient topologies in constructive set theory and type theory, Characterizing the interpretation of set theory in Martin-Löf type theory, Interfaces as functors, programs as coalgebras -- a final coalgebra theorem in intensional type theory, A type-theoretic approach to program development, FROM MULTISETS TO SETS IN HOMOTOPY TYPE THEORY, TYPED TIMED INPUT/OUTPUT AUTOMATA IN REAL-TIME, CYBERNETIC EXPLANATION, Introduction: Inferences and proofs, The seeming interdependence between the concepts of valid inference and proof, Dag Prawitz on proofs, operations and grounding, The neglect of epistemic considerations in logic: the case of epistemic assumptions, The justification of identity elimination in Martin-Löf's type theory, Proof, meaning and paradox: some remarks, Multisets in type theory, Type Theory Should Eat Itself, Another Look at Function Domains, A UNIVERSE OF STRICTLY POSITIVE FAMILIES, THE CONCEPTHORSEIS A CONCEPT, Can You Add Power‐Sets to Martin‐Lof's Intuitionistic Set Theory?, Constructive Versus Ontological Construals of Cantorian Ordinals, Constructive Galois Connections, C for constructivism. Beyond clichés, A Modular Type-Checking Algorithm for Type Theory with Singleton Types and Proof Irrelevance, Kripke Semantics for Martin-Löf’s Extensional Type Theory, Manifest Fields and Module Mechanisms in Intensional Type Theory, Equivalents of the finitary non-deterministic inductive definitions, Interactive computations: toward risk management in interactive intelligent systems, Proceeding in Abstraction. From Concepts to Types and the Recent Perspective on Information, Unnamed Item, From signatures to monads in \textsf{UniMath}, Factorization systems and fibrations, Containers: Constructing strictly positive types, Reflections on reflections in explicit mathematics, Machine-checked proof of the Church-Rosser theorem for the lambda calculus using the Barendregt variable convention in constructive type theory, Truth as an epistemic notion, Aspects of general topology in constructive set theory, Pretopologies and a uniform presentation of sup-lattices, quantales and frames, On the collection of points of a formal space, Steps towards a proof-theoretical semantics, Programming interfaces and basic topology, Maximal and partial points in formal spaces, Regular universes and formal spaces, Formal Zariski topology: Positivity and points, Indexed induction-recursion, A Framework for Defining Logical Frameworks, Lightweight Static Capabilities, Extensional equality preservation and verified generic programming, The axiom of multiple choice and models for constructive set theory
