4 citations · 10 across the 11 of their papers we have counts for
10 papers · 1 filter
Representing Continuous Functions between Greatest Fixed Points of Indexed Containers
Pierre Hyvernat
We describe a way to represent computable functions between coinductive types as particular transducers in type theory. This generalizes earlier work on functions between streams b…
Totality for Mixed Inductive and Coinductive Types
Pierre Hyvernat
This paper introduces an ML / Haskell like programming language with nested inductive and coinductive algebraic datatypes called \chariot. Functions are defined by arbitrary recurs…
A Linear Category of Polynomial Functors (extensional part)
Hyvernat Pierre
We construct a symmetric monoidal closed category of polynomial endofunctors (as objects) and simulation cells (as morphisms). This structure is defined using universal properties…
The Size-Change Termination Principle for Constructor Based Languages
Hyvernat Pierre
This paper describes an automatic termination checker for a generic first-order call-by-value language in ML style. We use the fact that value are built from variants and tuples to…
A Linear Category of Polynomial Diagrams
Pierre Hyvernat
We present a categorical model for intuitionistic linear logic where objects are polynomial diagrams and morphisms are simulation diagrams. The multiplicative structure (tensor pro…
Predicate Transformers, (co)Monads and Resolutions
Pierre Hyvernat
This short note contains random thoughts about a factorization theorem for closure/interior operators on a powerset which is reminiscent to the notion of resolution for a monad/com…