4 citations · 10 across the 11 of their papers we have counts for
11 papers
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…
Some Properties of Inclusions of Multisets and Contractive Boolean Operators
Pierre Hyvernat
Consider the following curious puzzle: call an n-tuple X=(X_1, ..., X_n) of sets smaller than another n-tuple Y if it has fewer //unordered sections//. We show that equivalence cla…