Lectures on the Curry-Howard isomorphism

Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations (03-02) Cut-elimination and normal-form theorems (03F05) Combinatory logic and lambda calculus (03B40) Logic in computer science (03B70) Functionals in proof theory (03F10)

Cited In (only showing first 100 items - show all)

Intuitionistic completeness of first-order logic
Self-referentiality of Brouwer-Heyting-Kolmogorov semantics
A constructive analysis of learning in Peano arithmetic
Existential type systems between Church and Curry style (type-free style)
Title not available (Why is that?)
Title not available (Why is that?)
On natural deduction in classical first-order logic: Curry-Howard correspondence, strong normalization and Herbrand's theorem
Axiomatic and dual systems for constructive necessity, a formally verified equivalence
A formal system of reduction paths for parallel reduction
Monoidal-closed categories of tree automata
In the full propositional logic, 5/8 of classical tautologies are intuitionistically valid
Unifying sets and programs via dependent types
Contribution of Warsaw logicians to computational logic
Second-order abstract categorial grammars as hyperedge replacement grammars
Introduction to Type Theory
Title not available (Why is that?)
An Alternative Natural Deduction for the Intuitionistic Propositional Logic
J-Calc: a typed lambda calculus for intuitionistic justification logic
The role of polymorphism in the characterisation of complexity by soft types
Brouwer's \(\epsilon\)-fixed point and Sperner's lemma
A semantic hierarchy for intuitionistic logic
A modal type theory for formalizing trusted communications
A computational interpretation of conceptivism
Partial algebras and complexity of satisfiability and universal theory for distributive lattices, Boolean algebras and Heyting algebras
An analytic calculus for the intuitionistic logic of proofs
The Church-Rosser theorem and quantitative analysis of witnesses
TWAM: a certifying abstract machine for logic programs
Tautologies over implication with negative literals
Completeness of second-order intuitionistic propositional logic with respect to phase semantics for proof-terms
Curry-Howard for incomplete first-order logic derivations using one-and-a-half level terms
KAT-ML: an interactive theorem prover for Kleene algebra with tests
On second order intuitionistic propositional logic without a universal quantifier
MATHEMATICAL RIGOR AND PROOF
When are different type-logical semantic definitions defining equivalent meanings?
Conjunctive, Disjunctive, Negative Objects and Generalized Quantification
Game semantics for the Lambek-calculus: Capturing directionality and the absence of structural rules
Delimited control operators prove double-negation shift
QUANTIFIED INTUITIONISTIC LOGIC OVER METRIZABLE SPACES
De Bruijn's weak diamond property revisited
Obituary: Nicolaas Govert de Bruijn (1918--2012). Mathematician, computer scientist, logician
What is the meaning of proofs?. A Fregean distinction in proof-theoretic semantics
Extracting \(\mathsf{BB'IW}\) inhabitants of simple types from proofs in the sequent calculus \(LT_\to^t\) for implicational ticket entailment
Homotopy-Theoretic Models of Type Theory
Reduction rules for intuitionistic \(\lambda\rho\)-calculus
COMPLETENESS OF SECOND-ORDER PROPOSITIONAL S4 AND H IN TOPOLOGICAL SEMANTICS
Intuitionistic games: determinacy, completeness, and normalization
Deriving a Floyd-Hoare logic for non-local jumps from a formulæ-as-types notion of control
A curious dialogical logic and its composition problem
Coalgebras in functional programming and type theory
Title not available (Why is that?)
In the Search of a Naive Type Theory
Answer set programming in intuitionistic logic
Existential Type Systems with No Types in Terms
Practical Proof Search for Coq by Type Inhabitation
Lewis meets Brouwer: constructive strict implication
Verificationism and Classical Realizability
Linear logic in computer science
A typed lambda calculus with intersection types
Categorial Grammars and Their Logics
A computer-verified monadic functional implementation of the integral
Title not available (Why is that?)
On the number of unary-binary tree-like structures with restrictions on the unary height
A coinductive approach to proof search through typed lambda-calculi
Constructive belief reports
Title not available (Why is that?)
Title not available (Why is that?)
Strong cut-elimination in sequent calculus using Klop's ι-translation and perpetual reductions
Dual and axiomatic systems for constructive S4, a formally verified equivalence
Towards logical foundations for probabilistic computation
Title not available (Why is that?)
Proof Terms for Generalized Natural Deduction
Algorithmic Theories of Problems. A Constructive and a Non-Constructive Approach
Complementary proof nets for classical logic
The New Normal: We Cannot Eliminate Cuts in Coinductive Calculi, But We Can Explore Them
Contextual modal type theory with polymorphic contexts
Title not available (Why is that?)
On measure quantifiers in first-order arithmetic
Title not available (Why is that?)
Topological quantum gates in homotopy type theory
The Significance of the Curry-Howard Isomorphism
Title not available (Why is that?)
Constructive forcing, CPS translations and witness extraction in Interactive realizability
Preserving cardinals and weak forms of Zorn’s lemma in realizability models
Implicit computation complexity in higher-order programming languages
A note on subject reduction in \((\to, \exists)\)-Curry with respect to complete developments
Truth, Proof, and Reproducibility: There’s No Counter-Attack for the Codeless
On interactive proof-search for constructive modal necessity
Intuitionistic Ancestral Logic as a Dependently Typed Abstract Programming Language
UNDER LOCK AND KEY: A PROOF SYSTEM FOR A MULTIMODAL LOGIC
On Higher-Order Probabilistic Subrecursion
Inhabitation of Low-Rank Intersection Types
Plotkin's call-by-value \(\lambda\)-calculus as a modal calculus
Combinatory logic with polymorphic types
How Hard Is Positive Quantification?
A note on synonymy in proof-theoretic semantics
The placeholder view of assumptions and the Curry-Howard correspondence
KURT GÖDEL ON LOGICAL, THEOLOGICAL, AND PHYSICAL ANTINOMIES
Dynamic game semantics
Justification logic and type theory as formalizations of intuitionistic propositional logic
Small model property reflects in games and automata

This page was built for publication: Lectures on the Curry-Howard isomorphism

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q881453)