2 citations · 3 across the 5 of their papers we have counts for
6 papers
An Intuitionistic Set-theoretical Model of Fully Dependent CCω
Masahiro Sato, Jacques Garrigue
Werner's set-theoretical model is one of the simplest models of CIC. It combines a functional view of predicative universes with a collapsed view of the impredicative sort Prop. Ho…
Formal Adventures in Convex and Conical Spaces
Reynald Affeldt, Jacques Garrigue, Takafumi Saikawa
Convex sets appear in various mathematical theories, and are used to define notions such as convex functions and hulls. As an abstraction from the usual definition of convex sets i…
A Trustful Monad for Axiomatic Reasoning with Probability and Nondeterminism
Reynald Affeldt, Jacques Garrigue, David Nowak +1
The algebraic properties of the combination of probabilistic choice and nondeterministic choice have long been a research topic in program semantics. This paper explains a formaliz…
Proving tree algorithms for succinct data structures
Reynald Affeldt, Jacques Garrigue, Xuanrui Qi +1
Succinct data structures give space-efficient representations of large amounts of data without sacrificing performance. They rely one cleverly designed data representations and alg…
GADTs and Exhaustiveness: Looking for the Impossible
Jacques Garrigue, Jacques Le Normand
Sound exhaustiveness checking of pattern-matching is an essential feature of functional programming languages, and OCaml supports it for GADTs. However this check is incomplete, in…
Proceedings ML Family/OCaml Users and Developers workshops
Oleg Kiselyov, Jacques Garrigue
This volume collects the extended versions of selected papers originally presented at the two ACM SIGPLAN workshops: ML Family Workshop 2014 and OCaml 2014. Both were affiliated wi…