From the 1 of 5.5k papers with an AI index.
29.3k citations
- Centre National de la Recherche ScientifiqueFR1.7k papers
- Centre Inria de SaclayFR364 papers
- École PolytechniqueFR306 papers
- Laboratoire Lorrain de Recherche en Informatique et ses ApplicationsFR300 papers
- École Normale Supérieure - PSLFR292 papers
- Sorbonne UniversitéFR291 papers
- École Normale Supérieure de LyonFR233 papers
- Centre Inria de l'Université Grenoble AlpesFR216 papers
- Université Paris-SaclayFR208 papers
- Université Grenoble AlpesFR204 papers
- Lyon 1 UniversitéFR191 papers
- Centre Inria d'Université Côte d'AzurFR183 papers
26 papers · 2 filters
The Biequivalence of Locally Cartesian Closed Categories and Martin-Löf Type Theories
Pierre Clairambault, Peter Dybjer
Seely's paper "Locally cartesian closed categories and type theory" contains a well-known result in categorical type theory: that the category of locally cartesian closed categorie…
Wave Equation Numerical Resolution: a Comprehensive Mechanized Proof of a C Program
Sylvie Boldo, Francois Clement, Jean-Christophe Filliâtre +3
We formally prove correct a C program that implements a numerical scheme for the resolution of the one-dimensional acoustic wave equation. Such an implementation introduces errors…
Proof-irrelevant model of CC with predicative induction and judgmental equality
Gyesik Lee, Benjamin Werner
We present a set-theoretic, proof-irrelevant model for Calculus of Constructions (CC) with predicative induction and judgmental equality in Zermelo-Fraenkel set theory with an axio…
From nominal sets binding to functions and lambda-abstraction: connecting the logic of permutation models with the logic of functions
Gilles Dowek, Murdoch Gabbay
Permissive-Nominal Logic (PNL) extends first-order predicate logic with term-formers that can bind names in their arguments. It takes a semantics in (permissive-)nominal sets. In P…
Coupling policy iteration with semi-definite relaxation to compute accurate numerical invariants in static analysis
Assalé Adjé, Stéphane Gaubert, Eric Goubault
We introduce a new domain for finding precise numerical invariants of programs by abstract interpretation. This domain, which consists of level sets of non-linear functions, genera…
Generalization Strategies for the Verification of Infinite State Systems
Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti +1
We present a method for the automated verification of temporal properties of infinite state systems. Our verification method is based on the specialization of constraint logic prog…