scientific article; zbMATH DE number 3365218

From MaRDI portal
Publication:5638283

zbMath0231.02040MaRDI QIDQ5638283

Per Martin-Löf

Publication date: 1971


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



Related Items

Inductive families, Logicality, double-line rules, and modalities, Cut-Elimination and Proof Schemata, Algorithmic Theories of Problems. A Constructive and a Non-Constructive Approach, Unnamed Item, Representing inductively defined sets by wellorderings in Martin-Löf's type theory, SUBATOMIC INFERENCES: AN INFERENTIALIST SEMANTICS FOR ATOMICS, PREDICATES, AND NAMES, A Survey of the Proof-Theoretic Foundations of Logic Programming, Cut elimination for a logic with induction and co-induction, Proof-theoretic harmony: towards an intensional account, Well-Partial Orderings and their Maximal Order Types, Partial inductive definitions, Restricting Initial Sequents: The Trade-Offs Between Identity, Contraction and Cut, From Mathesis Universalis to Provability, Computability, and Constructivity, Dialogues, Reasons and Endorsement, An intuitionistic version of Ramsey's theorem and its use in program termination, An intuitionistic theory of types with assumptions of high-arity variables, Equational theories for inductive types, Another proof of the intuitionistic Ramsey theorem, Partial inductive definitions as type-systems for \(\lambda\)-terms, On systems of definitions, induction and recursion, Type-theoretic interpretation of iterated, strictly positive inductive definitions, On the unity of duality, Dependent Types at Work, An introduction to univalent foundations for mathematicians, Some derived rules of intuitionistic second order arithmetic, The harmony of identity, Least and greatest fixed points in intuitionistic natural deduction, The justification of identity elimination in Martin-Löf's type theory, Proof, meaning and paradox: some remarks, On the Completeness of Dynamic Logic, Intuitionistic Podelski-Rybalchenko theorem and equivalence between inductive definitions and cyclic proofs, Failure of completeness in proof-theoretic semantics, Inductive Completeness of Logics of Programs, Prawitz, Proofs, and Meaning, Explaining Deductive Inference, Can You Add Power‐Sets to Martin‐Lof's Intuitionistic Set Theory?, Iterated Inductive Definitions Revisited, Theory of proofs (arithmetic and analysis), A new connective in natural deduction, and its application to quantum computing, Uniform Inductive Reasoning in Transitive Closure Logic via Infinite Descent, Non-well-founded deduction for induction and coinduction, Lexicographic Path Induction, Cut-elimination for a logic with definitions and induction, An Approach to General Proof Theory and a Conjecture of a Kind of Completeness of Intuitionistic Logic Revisited, Integrating induction and coinduction via closure operators and proof cycles