About me

I'm a Postdoctoral Research Associate at Carnegie Mellon University in Qatar. I'm working in the Meta-CLF project. Previously, I was a Phd student in the Marelle team at INRIA Sophia-Antipolis. My research interests include Type Theory, type-based termination and computational logic.

Contact

Address : Carnegie Mellon University - Qatar Campus
P.O. Box 24866
Doha, Qatar
E-mail: sacchini [at] qatar [dot] cmu [dot] edu
Phone:+974 4454 8628

Publications

[1] Benjamin Grégoire and Jorge Luis Sacchini. On strong normalization of the calculus of constructions with type-based termination. In Christian G. Fermüller and Andrei Voronkov, editors, LPAR (Yogyakarta), volume 6397 of Lecture Notes in Computer Science, pages 333-347. Springer, 2010. [ Long version | .pdf ]
[2] Bruno Barras, Pierre Corbineau, Benjamin Grégoire, Hugo Herbelin, and Jorge Luis Sacchini. A new elimination rule for the Calculus of Inductive Constructions. In Stefano Berardi, Ferruccio Damiani, and Ugo de'Liguoro, editors, TYPES, volume 5497 of Lecture Notes in Computer Science, pages 32-48. Springer, 2008. [ .pdf ]
[3] Gilles Barthe, César Kunz, and Jorge Luis Sacchini. Certified reasoning in memory hierarchies. In G. Ramalingam, editor, APLAS, volume 5356 of Lecture Notes in Computer Science, pages 75-90. Springer, 2008. [ .pdf ]
[4] Benjamin Grégoire and Jorge Luis Sacchini. Combining a verification condition generator for a bytecode language with static analyses. In Gilles Barthe and Cédric Fournet, editors, TGC, volume 4912 of Lecture Notes in Computer Science, pages 23-40. Springer, 2007. [ code | .pdf ]

In BibTex