17 citations · 73 across the 11 of their papers we have counts for
11 papers
Pragmatic isomorphism proofs between Coq representations: application to lambda-term families
Catherine Dubois, Nicolas Magaud, Alain Giorgetti
There are several ways to formally represent families of data, such as lambda terms, in a type theory such as the dependent type theory of Coq. Mathematical representations are ver…
Multi-qubit doilies: enumeration for all ranks and classification for ranks four and five
Axel Muller, Metod Saniga, Alain Giorgetti +2
For , an -qubit doily is a doily living in the -qubit symplectic polar space. These doilies are related to operator-based proofs of quantum contextuality. Following…
Contextuality degree of quadrics in multi-qubit symplectic polar spaces
Henri de Boutray, Frédéric Holweck, Alain Giorgetti +2
Quantum contextuality takes an important place amongst the concepts of quantum computing that bring an advantage over its classical counterpart. For a large class of contextuality…
Taxonomy of Polar Subspaces of Multi-Qubit Symplectic Polar Spaces of Small Rank
Metod Saniga, Henri de Boutray, Frederic Holweck +1
We study certain physically-relevant subgeometries of binary symplectic polar spaces of small rank , when the points of these spaces canonically encode -qubit obs…
Your Proof Fails? Testing Helps to Find the Reason
Guillaume Petiot, Nikolai Kosmatov, Bernard Botella +2
Applying deductive verification to formally prove that a program respects its formal specification is a very complex and time-consuming task due in particular to the lack of feedba…
A correspondence between rooted planar maps and normal planar lambda terms
Noam Zeilberger, Alain Giorgetti
A rooted planar map is a connected graph embedded in the 2-sphere, with one edge marked and assigned an orientation. A term of the pure lambda calculus is said to be linear if ever…
Constructing large tables of numbers of maps by orientable genus
Alain Giorgetti, Timothy R. S. Walsh
The Carrell-Chapuy recurrence formulas dramatically improve the efficiency of counting orientable rooted maps by genus, either by number of edges alone or by number of edges and ve…
Quantum contextual finite geometries from dessins d'enfants
Michel Planat, Alain Giorgetti, Frédéric Holweck +1
We point out an explicit connection between graphs drawn on compact Riemann surfaces defined over the field of algebraic numbers --- so-called Grothendieck's {\i…
Lazy AC-Pattern Matching for Rewriting
Walid Belkhir, Alain Giorgetti
We define a lazy pattern-matching mechanism modulo associativity and commutativity. The solutions of a pattern-matching problem are stored in a lazy list composed of a first substi…
A Symbolic Transformation Language and its Application to a Multiscale Method
Walid Belkhir, Alain Giorgetti, Michel Lenczner
The context of this work is the design of a software, called MEMSALab, dedicated to the automatic derivation of multiscale models of arrays of micro- and nanosystems. In this domai…
Graph Based Reduction of Program Verification Conditions
Jean-François Couchot, Alain Giorgetti, Nicolas Stouls
Increasing the automaticity of proofs in deductive verification of C programs is a challenging task. When applied to industrial C programs known heuristics to generate simpler veri…