The Implicit Calculus of Constructions as a Programming Language with Dependent Types. - Bruno Barras; Bruno Bernardo (FoSSaCS, 2008)

Un Calcul des Constructions implicite avec sommes dépendantes et à inférence de type décidable. (An implicit Calculus of Constructions with dependent sums and decidable type inference). - Bruno Bernardo (2015)

Mi-Cho-Coq, a Framework for Certifying Tezos Smart Contracts. - Bruno Bernardo; Raphaël Cauderlier; Zhenlei Hu; Basile Pesin; Julien Tesson (FM Workshops (1), 2019)

Albert, An Intermediate Smart-Contract Language for the Tezos Blockchain. - Bruno Bernardo; Raphaël Cauderlier; Basile Pesin; Julien Tesson (Financial Cryptography Workshops, 2020)

Making Tezos Smart Contracts More Reliable with Coq. - Bruno Bernardo; Raphaël Cauderlier; Guillaume Claret; Arvid Jakobsson; Basile Pesin; Julien Tesson (ISoLA (3), 2020)