7 citations · 12 across the 6 of their papers we have counts for
7 papers
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…
Coinduction in Uniform: Foundations for Corecursive Proof Search with Horn Clauses
Henning Basold, Ekaterina Komendantskaya, Yue Li
We establish proof-theoretic, constructive and coalgebraic foundations for proof search in coinductive Horn clause theories. Operational semantics of coinductive Horn clause resolu…
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…
Dependent Inductive and Coinductive Types are Fibrational Dialgebras
Henning Basold
In this paper, I establish the categorical structure necessary to interpret dependent inductive and coinductive types. It is well-known that dependent type theories à la Martin-Löf…