Publications

Giuseppe Castagna, Mickaël Laurent & Kim Nguyen
We present a type system that combines, in a controlled way, first-order polymorphism with intersectiontypes, union types, and subtyping, and prove its safety. This makes the system a prime candidate to type dynamic languages.

Set-theoretic types Semantic subtyping Intersection types Union types Occurrence typing Type narrowing Dynamic language Type inference Polymorphism

Giuseppe Castagna, Mickaël Laurent, Kim Nguyen & Matthew Lutze
We extend classic union and intersection type systems with a type-case construction and show that the combination of the union elimination rule of the former and the typing rules for type-cases of our extension encompasses occurrence typing.

Set-theoretic types Semantic subtyping Intersection types Union types Occurrence typing Union elimination Typecases Type inference

Giuseppe Castagna, Victor Lanvin, Mickaël Laurent & Kim Nguyen
We revisit occurrence typing, a technique to refine the type of variables occurring in type-cases and, thus, capture some programming patterns used in untyped languages.

Set-theoretic types Semantic subtyping Occurrence typing Gradual typing Typecases

Daniel Larraz, Mickaël Laurent & Cesare Tinelli
We introduce two new major features of the open-source model checker Kind 2 which provide traceability information between specification and design elements such as assumptions, guarantees, or other behavioral constraints in synchronous reactive system models.

Model checking SMT Traceability Inductive validity cores Minimal cut sets