Recherche - Archive ouverte HAL Accéder directement au contenu

Filtrer vos résultats

12 résultats
Page :
triés par
Image document

A Semi-automatic Proof of Strong connectivity

 Ran Chen , Jean-Jacques Lévy
9th Working Conference on Verified Software: Theories, Tools and Experiments (VSTTE), Jul 2017, Heidelberg, Germany
Communication dans un congrès hal-01632947v1
Image document

Une preuve formelle de l'algorithme de Tarjan-1972 pour trouver les composantes fortement connexes dans un graphe

 Ran Chen , Jean-Jacques Lévy
JFLA 2017 - Vingt-huitièmes Journées Francophones des Langages Applicatifs, Jan 2017, Gourette, France
Communication dans un congrès hal-01422215v1
Image document

Confluence properties of weak and strong calculi of explicit substitutions

 P.L. Curien , Thérèse Hardin , Jean-Jacques Levy
[Research Report] RR-1617, INRIA. 1992
Rapport inria-00077189v1
Image document

Formal Proofs of Tarjan's Algorithm in Why3, Coq, and Isabelle

 Ran Chen , Cyril Cohen , Jean-Jacques Levy , Stephan Merz , Laurent Thery
2018
Pré-publication, Document de travail hal-01906155v1
Image document

Formal proofs of two algorithms for strongly connected components in graphs

 Ran Chen , Jean-Jacques Levy
2016
Pré-publication, Document de travail hal-01422216v1
Image document

Explicit substitutions

 Martin Abadi , Luca Cardelli , P.L. Curien , Jean-Jacques Levy
RR-1176, INRIA. 1990
Rapport inria-00075382v1
Image document

Finite Develpments in the Lambda Calculus

 Jean-Jacques Levy
Doctoral. Spain. 2021
Cours hal-03566512v1
Image document

Full abstraction for sequential languages : The states of the art

 Gérard Berry , Pierre-Louis Curien , Jean-Jacques Levy
[Research Report] RR-0197, INRIA. 1983
Rapport inria-00076361v1
Image document

Formal Proofs of Tarjan's Strongly Connected Components Algorithm in Why3, Coq and Isabelle

 Ran Chen , Cyril Cohen , Jean-Jacques Levy , Stephan Merz , Laurent Théry
ITP 2019 - 10th International Conference on Interactive Theorem Proving, Sep 2019, Portland, United States. pp.13:1 - 13:19, ⟨10.4230/LIPIcs.ITP.2019.13⟩
Communication dans un congrès hal-02303987v1
Image document

Readable semi-automatic formal proofs of Depth-First Search in graphs using Why3

 Ran Chen , Jean-Jacques Levy
2015
Pré-publication, Document de travail hal-01253136v1
Image document

Le systeme LUCIFER d'aide a la conception de circuits integres

 J. Chailloux , J.M. Hullot , Jean-Jacques Levy , J. Vuillemin
RR-0196, INRIA. 1983
Rapport inria-00076362v1
Image document

Tracking Redexes in the Lambda Calculus

 Jean-Jacques Levy
2022
Pré-publication, Document de travail hal-03564707v1
Page :