Proof theory in the abstract

DOI10.1016/S0168-0072(01)00075-6zbMath1007.03056WikidataQ126388056 ScholiaQ126388056MaRDI QIDQ5957852

J. M. E. Hyland

Publication date: 22 March 2003

Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)

zbMATH Keywords

Dialectica interpretationcategorical proof theory

Mathematics Subject Classification ID

Categorical logic, topoi (03G30) Structure of proofs (03F07) Proof-theoretic aspects of linear logic and other substructural logics (03F52) Functionals in proof theory (03F10)

Related Items

The 2-Chu-Dialectica construction and the polycategory of multivariable adjunctions, Bifibrations of polycategories and classical linear logic, Categorical proof theory of classical propositional calculus, Glueing and orthogonality for models of linear logic, Dialectica principles via Gödel doctrines, LNL polycategories and doctrines of linear logic, CHAD for expressive total languages, Polycategories via pseudo-distributive laws, On rectification and enrichment of infinity properads, Mathematical logic: proof theory, constructive mathematics. Abstracts from the workshop held November 5--11, 2017, Some reasons for generalising domain theory, Towards Hilbert's 24th Problem: Combinatorial Proof Invariants, On categorical models of classical logic and the Geometry of Interaction, Cartesian closed Dialectica categories, The problem of proof identity, and why computer scientists should care about Hilbert's 24th problem, Monoidal-closed categories of tree automata, Functional Interpretations of Intuitionistic Linear Logic, Dwyer–Kan homotopy theory for cyclic operads, Order-enriched categorical models of the classical sequent calculus

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Linear logic
• Weakly distributive categories
• On the unity of logic
• Natural deduction and coherence for weakly distributive categories
• Categorical logic and type theory
• Full intuitionistic linear logic
• Premonoidal categories as categories with algebraic structure
• A note on full intuitionistic linear logic
• Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
• Control categories and duality: on the categorical semantics of the lambda-mu calculus
• ÜBER EINE BISHER NOCH NICHT BENÜTZTE ERWEITERUNG DES FINITEN STANDPUNKTES
• A new constructive logic: classic logic
• Polycategories
• Categories for Types
• Premonoidal categories and notions of computation
• Eine Variante zur Dialectica-Interpretation der Heyting-Arithmetik endlicher Typen
• Realizability: a historical essay