On Recursive Functions and Well-Founded Relations in the Calculus of Constructions. - José Luis Freire; Enrique Freire Brañas; Antonio Blanco (EUROCAST, 2005)

On the Representation of Imperative Programs in a Logical Framework. - José Luis Freire-Nistal; Enrique Freire Brañas; Antonio Blanco Ferro; David Cabrero Souto (EUROCAST, 2007)

The Foldl Operator as a Coequalizer Using Coq. - Antonio Blanco; Enrique Freire Brañas; José Luis Freire; Javier París (EUROCAST, 2009)

On the Confluence of the Graphic Calculus with Penrose Diagrams (I). - José Luis Freire-Nistal; Antonio Blanco Ferro; J. M. Molinelli Barba; Enrique Freire Brañas (EUROCAST (1), 2011)