Embedding a logical theory of constructions in Agda. - Ana Bove; Peter Dybjer; Andrés Sicard-Ramírez (PLPV, 2009)

Combining Interactive and Automatic Reasoning in First Order Theories of Functional Programs. - Ana Bove; Peter Dybjer; Andrés Sicard-Ramírez (FoSSaCS, 2012)

About Opposition and Duality in Paraconsistent Type Theory. - Juan Carlos Agudelo Agudelo; Andrés Sicard-Ramírez (LSFA, 2021)

Type Theory with Opposite Types: A Paraconsistent Type Theory. - Juan Carlos Agudelo Agudelo; Andrés Sicard-Ramírez (Log. J. IGPL, 2022)