Pages that link to "Item:Q881453"
From MaRDI portal
The following pages link to Lectures on the Curry-Howard isomorphism (Q881453):
Displaying 50 items.
- On natural deduction in classical first-order logic: Curry-Howard correspondence, strong normalization and Herbrand's theorem (Q265002) (← links)
- J-Calc: a typed lambda calculus for intuitionistic justification logic (Q276037) (← links)
- The role of polymorphism in the characterisation of complexity by soft types (Q276263) (← links)
- Intuitionistic games: determinacy, completeness, and normalization (Q332080) (← links)
- Partial algebras and complexity of satisfiability and universal theory for distributive lattices, Boolean algebras and Heyting algebras (Q391322) (← links)
- Intuitionistic completeness of first-order logic (Q392280) (← links)
- Self-referentiality of Brouwer-Heyting-Kolmogorov semantics (Q392298) (← links)
- Existential type systems between Church and Curry style (type-free style) (Q402117) (← links)
- Unifying sets and programs via dependent types (Q408534) (← links)
- In the full propositional logic, 5/8 of classical tautologies are intuitionistically valid (Q408542) (← links)
- A modal type theory for formalizing trusted communications (Q420842) (← links)
- When are different type-logical semantic definitions defining equivalent meanings? (Q439958) (← links)
- Deriving a Floyd-Hoare logic for non-local jumps from a formulæ-as-types notion of control (Q444460) (← links)
- A constructive analysis of learning in Peano arithmetic (Q450942) (← links)
- Delimited control operators prove double-negation shift (Q450950) (← links)
- A curious dialogical logic and its composition problem (Q484198) (← links)
- Constructive belief reports (Q514084) (← links)
- Brouwer's \(\epsilon\)-fixed point and Sperner's lemma (Q549181) (← links)
- Coalgebras in functional programming and type theory (Q639643) (← links)
- Pedagogical second-order \(\lambda \)-calculus (Q732007) (← links)
- Obituary: Nicolaas Govert de Bruijn (1918--2012). Mathematician, computer scientist, logician (Q740456) (← links)
- De Bruijn's weak diamond property revisited (Q740482) (← links)
- Reduction rules for intuitionistic \(\lambda\rho\)-calculus (Q897480) (← links)
- A typed lambda calculus with intersection types (Q930870) (← links)
- Curry-Howard for incomplete first-order logic derivations using one-and-a-half level terms (Q964000) (← links)
- Second-order abstract categorial grammars as hyperedge replacement grammars (Q972434) (← links)
- A computer-verified monadic functional implementation of the integral (Q987984) (← links)
- Game semantics for the Lambek-calculus: Capturing directionality and the absence of structural rules (Q1005955) (← links)
- The Church-Rosser theorem and quantitative analysis of witnesses (Q1627965) (← links)
- TWAM: a certifying abstract machine for logic programs (Q1629962) (← links)
- Lewis meets Brouwer: constructive strict implication (Q1688950) (← links)
- Answer set programming in intuitionistic logic (Q1688962) (← links)
- A semantic hierarchy for intuitionistic logic (Q1740610) (← links)
- On the number of unary-binary tree-like structures with restrictions on the unary height (Q1745901) (← links)
- A formal system of reduction paths for parallel reduction (Q1989338) (← links)
- Completeness of second-order intuitionistic propositional logic with respect to phase semantics for proof-terms (Q2000674) (← links)
- What is the meaning of proofs?. A Fregean distinction in proof-theoretic semantics (Q2037304) (← links)
- Curry-Howard-Lambek correspondence for intuitionistic belief (Q2062203) (← links)
- On measure quantifiers in first-order arithmetic (Q2117748) (← links)
- On interactive proof-search for constructive modal necessity (Q2133450) (← links)
- Plotkin's call-by-value \(\lambda\)-calculus as a modal calculus (Q2141293) (← links)
- Combinatory logic with polymorphic types (Q2144609) (← links)
- Justification logic and type theory as formalizations of intuitionistic propositional logic (Q2151394) (← links)
- Small model property reflects in games and automata (Q2151424) (← links)
- Linear logic in computer science (Q2201109) (← links)
- Dual and axiomatic systems for constructive S4, a formally verified equivalence (Q2219076) (← links)
- A coinductive approach to proof search through typed lambda-calculi (Q2231698) (← links)
- Extracting \(\mathsf{BB'IW}\) inhabitants of simple types from proofs in the sequent calculus \(LT_\to^t\) for implicational ticket entailment (Q2254561) (← links)
- On paradoxes in normal form (Q2288281) (← links)
- An analytic calculus for the intuitionistic logic of proofs (Q2330501) (← links)
