4 papers · 1 filter
Session Coalgebras: A Coalgebraic View on Session Types and Communication Protocols
Alex C. Keizer, Henning Basold, Jorge A. Pérez
Compositional methods are central to the development and verification of software systems. They allow to break down large systems into smaller components, while enabling reasoning…
The New Normal: We Cannot Eliminate Cuts in Coinductive Calculi, But We Can Explore Them
Ekaterina Komendantskaya, Dmitry Rozplokhas, Henning Basold
In sequent calculi, cut elimination is a property that guarantees that any provable formula can be proven analytically. For example, Gentzen's classical and intuitionistic calculi…
Breaking the Loop: Recursive Proofs for Coinductive Predicates in Fibrations
Henning Basold
The purpose of this paper is to develop and study recursive proofs of coinductive predicates. Such recursive proofs allow one to discover proof goals in the construction of a proof…
Type Theory based on Dependent Inductive and Coinductive Types
Henning Basold, Herman Geuvers
We develop a dependent type theory that is based purely on inductive and coinductive types, and the corresponding recursion and corecursion principles. This results in a type theor…