16 citations · 57 across the 9 of their papers we have counts for
10 papers
A Reasonably Gradual Type Theory
Kenji Maillard, Meven Lennon-Bertrand, Nicolas Tabareau +1
Gradualizing the Calculus of Inductive Constructions (CIC) involves dealing with subtle tensions between normalization, graduality, and conservativity with respect to CIC. Recently…
The Multiverse: Logical Modularity for Proof Assistants
Kenji Maillard, Nicolas Margulies, Matthieu Sozeau +2
Proof assistants play a dual role as programming languages and logical systems. As programming languages, proof assistants offer standard modularity mechanisms such as first-class…
Gradualizing the Calculus of Inductive Constructions
Meven Lennon-Bertrand, Kenji Maillard, Nicolas Tabareau +1
We investigate gradual variations on the Calculus of Inductive Construction (CIC) for swifter prototyping with imprecise types and terms. We observe, with a no-go theorem, a crucia…
The Marriage of Univalence and Parametricity
Nicolas Tabareau, Éric Tanter, Matthieu Sozeau
Reasoning modulo equivalences is natural for everyone, including mathematicians. Unfortunately, in proof assistants based on type theory, equality is appallingly syntactic and, as…
Gradual Certified Programming in Coq
Éric Tanter, Nicolas Tabareau
Expressive static typing disciplines are a powerful way to achieve high-quality software. However, the adoption cost of such techniques should not be under-estimated. Just like gra…
Contraction analysis of nonlinear random dynamical systems
Nicolas Tabareau, Jean-Jacques Slotine
In order to bring contraction analysis into the very fruitful and topical fields of stochastic and Bayesian systems, we extend here the theory describes in \cite{Lohmiller98} to ra…