Sequent Calculus in the Topos of Trees

DOI10.1007/978-3-662-46678-0_9zbMath1461.03060arXiv1501.03293OpenAlexW1603328070MaRDI QIDQ2948556

Ranald Clouston, Rajeev Goré

Publication date: 1 October 2015

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1501.03293

Mathematics Subject Classification ID

Categorical logic, topoi (03G30) Cut-elimination and normal-form theorems (03F05) Proof theory in general (including proof-theoretic semantics) (03F03)

Related Items

Lewis meets Brouwer: constructive strict implication, The Guarded Lambda-Calculus: Programming and Reasoning with Guarded Recursion for Coinductive Types, Coinduction in Flow: The Later Modality in Fibrations