Combining a Verification Condition Generator for a Bytecode Language with Static Analyses. - Benjamin Grégoire; Jorge Luis Sacchini (TGC, 2007)

Certified Reasoning in Memory Hierarchies. - Gilles Barthe; César Kunz; Jorge Luis Sacchini (APLAS, 2008)

A New Elimination Rule for the Calculus of Inductive Constructions. - Bruno Barras; Pierre Corbineau; Benjamin Grégoire; Hugo Herbelin; Jorge Luis Sacchini (TYPES, 2008)

On Strong Normalization of the Calculus of Constructions with Type-Based Termination. - Benjamin Grégoire; Jorge Luis Sacchini (LPAR (Yogyakarta), 2010)

Type-Based Productivity of Stream Definitions in the Calculus of Constructions. - Jorge Luis Sacchini (LICS, 2013)

Towards Meta-Reasoning in the Concurrent Logical Framework CLF. - Iliano Cervesato; Jorge Luis Sacchini (EXPRESS/SOS, 2013)

Linear Sized Types in the Calculus of Constructions. - Jorge Luis Sacchini (FLOPS, 2014)

Combining Mechanized Proofs and Model-Based Testing in the Formal Analysis of a Hypervisor. - Hanno Becker; Juan Manuel Crespo; Jacek Galowicz; Ulrich Hensel; Yoichi Hirai; César Kunz; Keiko Nakata 001; Jorge Luis Sacchini; Hendrik Tews; Thomas Tuerk (FM, 2016)