About me

I'm a Postdoctoral Research Associate at Carnegie Mellon University in Qatar. I'm working in the Coq^ project. I was also a member of the Meta-CLF project. My research interests include Type Theory, type-based termination and computational logic.

Before joining CMU-Q, I was a PhD student of Benjamin Grégoire in the Marelle team at INRIA Sophia-Antipolis.

Here is my CV.

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

Projects

Meta-CLF : Formal reasoning about languages for distributed computation.
Coq^ : Type-based termination in the Coq proof assistant.

Thesis

On Type-Based Termination and Dependent Pattern Matching in the Calculus of Inductive Constructions

Defended on June 29th, 2011. Details here.

PDF copy at HAL.

Publications

[1] Jorge Luis Sacchini. Linear Sized Types in the Calculus of Constructions. In FLOPS, 2014. [ .pdf ]
[2] Iliano Cervesato and Jorge Luis Sacchini. Towards meta-reasoning in the concurrent logical framework CLF. In Johannes Borgström and Bas Luttik, editors, EXPRESS/SOS, volume 120 of EPTCS, 2013. [ .pdf ]
[3] Jorge Luis Sacchini. Type-Based Productivity of Stream Definitions in the Calculus of Constructions. In LICS, pages 233–242. IEEE Computer Society, 2013. [ .pdf ]
[4] Iliano Cervesato, Frank Pfenning, Jorge Luis Sacchini, Carsten Schürmann, and Robert J. Simmons. Trace Matching in a Concurrent Logical Framework. In Adam Chlipala and Carsten Schürmann, editors, 7th International Workshop on Logical Frameworks and Meta-languages: Theory and Practice - LFMTP'12, Copenhagen, Denmark, September 2012. [ .pdf ]
[5] Iliano Cervesato, Frank Pfenning, Jorge Luis Sacchini, Carsten Schürmann, and Robert J. Simmons. On Matching Concurrent Traces. In Santiago Escobar, Konstantin Korovin, and Vladimir Rybakov, editors, 26th International Workshop on Unification - UNIF'12, Manchester, UK, July 2012. [ .pdf ]
[6] Iliano Cervesato, Frank Pfenning, Jorge Luis Sacchini, Carsten Schürmann, and Robert J. Simmons. On Matching in CLF. Technical Report CMU-CS-12-114, Department of Computer Science, Carnegie Mellon University, Pittsburgh, PA, July 2012. [ .pdf ]
[7] 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, Logic for Programming, Artificial Intelligence, and Reasoning - 17th International Conference, LPAR-17, Yogyakarta, Indonesia, October 10-15, 2010. Proceedings, volume 6397 of Lecture Notes in Computer Science, pages 333-347. Springer, 2010. [ Long version | .pdf ]
[8] 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 for Proofs and Programs, International Conference, TYPES 2008, Torino, Italy, March 26-29, 2008, Revised Selected Papers, volume 5497 of Lecture Notes in Computer Science, pages 32-48. Springer, 2008. [ .pdf ]
[9] Gilles Barthe, César Kunz, and Jorge Luis Sacchini. Certified reasoning in memory hierarchies. In G. Ramalingam, editor, Programming Languages and Systems, 6th Asian Symposium, APLAS 2008, Bangalore, India, December 9-11, 2008. Proceedings, volume 5356 of Lecture Notes in Computer Science, pages 75-90. Springer, 2008. [ .pdf ]
[10] 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, Trustworthy Global Computing, Third Symposium, TGC 2007, Sophia-Antipolis, France, November 5-6, 2007, Revised Selected Papers, volume 4912 of Lecture Notes in Computer Science, pages 23-40. Springer, 2007. [ code | .pdf ]

In BibTex

Software