Lectures on the Curry-Howard isomorphism
From MaRDI portal
Publication:881453
zbMath1183.03004MaRDI QIDQ881453
Paweł Urzyczyn, Morten Heine B. Sørensen
Publication date: 30 May 2007
Published in: Studies in Logic and the Foundations of Mathematics (Search for Journal in Brave)
reductionpolymorphismtypenormalizationlambda calculusproofcontrol operatordependent typepure type system
Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations (03-02) Logic in computer science (03B70) Cut-elimination and normal-form theorems (03F05) Functionals in proof theory (03F10) Combinatory logic and lambda calculus (03B40)
Related Items (only showing first 100 items - show all)
Normalization in the simply typed -calculus ⋮ A Survey of the Proof-Theoretic Foundations of Logic Programming ⋮ A correct-by-construction conversion from lambda calculus to combinatory logic ⋮ The placeholder view of assumptions and the Curry-Howard correspondence ⋮ A dialogical route to logical pluralism ⋮ On counting propositional logic and Wagner's hierarchy ⋮ The existential fragment of second-order propositional intuitionistic logic is undecidable ⋮ Complementary proof nets for classical logic ⋮ UNDER LOCK AND KEY: A PROOF SYSTEM FOR A MULTIMODAL LOGIC ⋮ Game semantics of Martin-Löf type theory ⋮ Node Replication: Theory And Practice ⋮ Core Type Theory ⋮ Unnamed Item ⋮ Proof Terms for Generalized Natural Deduction ⋮ Implicit computation complexity in higher-order programming languages ⋮ On natural deduction in classical first-order logic: Curry-Howard correspondence, strong normalization and Herbrand's theorem ⋮ How Hard Is Positive Quantification? ⋮ J-Calc: a typed lambda calculus for intuitionistic justification logic ⋮ The role of polymorphism in the characterisation of complexity by soft types ⋮ The Church-Rosser theorem and quantitative analysis of witnesses ⋮ On interactive proof-search for constructive modal necessity ⋮ TWAM: a certifying abstract machine for logic programs ⋮ Practical Proof Search for Coq by Type Inhabitation ⋮ Plotkin's call-by-value \(\lambda\)-calculus as a modal calculus ⋮ Combinatory logic with polymorphic types ⋮ Unnamed Item ⋮ Justification logic and type theory as formalizations of intuitionistic propositional logic ⋮ Small model property reflects in games and automata ⋮ Intuitionistic games: determinacy, completeness, and normalization ⋮ Unnamed Item ⋮ Monotone recursive types and recursive data representations in Cedille ⋮ Algorithmic Theories of Problems. A Constructive and a Non-Constructive Approach ⋮ MATHEMATICAL RIGOR AND PROOF ⋮ A computational interpretation of conceptivism ⋮ Partial algebras and complexity of satisfiability and universal theory for distributive lattices, Boolean algebras and Heyting algebras ⋮ Intuitionistic completeness of first-order logic ⋮ Self-referentiality of Brouwer-Heyting-Kolmogorov semantics ⋮ Intuitionistic Ancestral Logic as a Dependently Typed Abstract Programming Language ⋮ In the Search of a Naive Type Theory ⋮ Existential type systems between Church and Curry style (type-free style) ⋮ Realist Consequence, Epistemic Inference, Computational Correctness ⋮ Lewis meets Brouwer: constructive strict implication ⋮ Answer set programming in intuitionistic logic ⋮ Unifying sets and programs via dependent types ⋮ In the full propositional logic, 5/8 of classical tautologies are intuitionistically valid ⋮ Contribution of Warsaw logicians to computational logic ⋮ An Alternative Natural Deduction for the Intuitionistic Propositional Logic ⋮ Reduction rules for intuitionistic \(\lambda\rho\)-calculus ⋮ A modal type theory for formalizing trusted communications ⋮ Constructive forcing, CPS translations and witness extraction in Interactive realizability ⋮ Linear logic in computer science ⋮ The placeholder view of assumptions and the Curry-Howard correspondence (extended abstract) ⋮ When are different type-logical semantic definitions defining equivalent meanings? ⋮ Coalgebras in functional programming and type theory ⋮ Ordered combinatory algebras and realizability ⋮ Unnamed Item ⋮ Deriving a Floyd-Hoare logic for non-local jumps from a formulæ-as-types notion of control ⋮ Categorial Grammars and Their Logics ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ A constructive analysis of learning in Peano arithmetic ⋮ Delimited control operators prove double-negation shift ⋮ Dual and axiomatic systems for constructive S4, a formally verified equivalence ⋮ On Higher-Order Probabilistic Subrecursion ⋮ Unnamed Item ⋮ A typed lambda calculus with intersection types ⋮ The New Normal: We Cannot Eliminate Cuts in Coinductive Calculi, But We Can Explore Them ⋮ A curious dialogical logic and its composition problem ⋮ Conjunctive, Disjunctive, Negative Objects and Generalized Quantification ⋮ Can a Quantum Computer Run the von Neumann Architecture? ⋮ A coinductive approach to proof search through typed lambda-calculi ⋮ Verificationism and Classical Realizability ⋮ Truth, Proof, and Reproducibility: There’s No Counter-Attack for the Codeless ⋮ A semantic hierarchy for intuitionistic logic ⋮ Homotopy-Theoretic Models of Type Theory ⋮ On the number of unary-binary tree-like structures with restrictions on the unary height ⋮ A formal system of reduction paths for parallel reduction ⋮ Constructive belief reports ⋮ Completeness of second-order intuitionistic propositional logic with respect to phase semantics for proof-terms ⋮ Extracting \(\mathsf{BB'IW}\) inhabitants of simple types from proofs in the sequent calculus \(LT_\to^t\) for implicational ticket entailment ⋮ Curry-Howard for incomplete first-order logic derivations using one-and-a-half level terms ⋮ Tautologies over implication with negative literals ⋮ Second-order abstract categorial grammars as hyperedge replacement grammars ⋮ Brouwer's \(\epsilon\)-fixed point and Sperner's lemma ⋮ Introduction to Type Theory ⋮ Unnamed Item ⋮ A computer-verified monadic functional implementation of the integral ⋮ Unnamed Item ⋮ Unifying Sets and Programs via Dependent Types ⋮ What is the meaning of proofs?. A Fregean distinction in proof-theoretic semantics ⋮ On paradoxes in normal form ⋮ On second order intuitionistic propositional logic without a universal quantifier ⋮ Strong cut-elimination in sequent calculus using Klop's ι-translation and perpetual reductions ⋮ Strong Normalisation of Cut-Elimination That Simulates β-Reduction ⋮ Game semantics for the Lambek-calculus: Capturing directionality and the absence of structural rules ⋮ COMPLETENESS OF SECOND-ORDER PROPOSITIONAL S4 AND H IN TOPOLOGICAL SEMANTICS ⋮ Unnamed Item ⋮ Obituary: Nicolaas Govert de Bruijn (1918--2012). Mathematician, computer scientist, logician ⋮ De Bruijn's weak diamond property revisited
This page was built for publication: Lectures on the Curry-Howard isomorphism
