A proof system for a sequential object-based language. - Carlos Camarao de Figueiredo (1995)

Towards Higher-Order Types. - Carlos Camarão 001; Lucília Figueiredo (US-Brazil Joint Workshops on the Formal Foundations of Software Systems, 1997)

A Type System for Context-dependent Overloading. - Carlos Camarão 001; Lucília Figueiredo (US-Brazil Joint Workshops on the Formal Foundations of Software Systems, 1997)

Type Inference for Overloading without Restrictions, Declarations or Annotations. - Carlos Camarão 001; Lucília Figueiredo (Fuji International Symposium on Functional and Logic Programming, 1999)

Adapting Web Contents to WAP Devices using Haskell. - Pedro Ivo Oliveira; Carlos Camarão 001 (SCCC, 2001)

A View on Abstract and Extensibles Types. - Lucília Figueiredo; Carlos Camarão 001 (Rev. Colomb. de Computación, 2002)

Mimico: a Monad Combinator Parser Generator. - Carlos Camarão 001; Lucília Figueiredo; Hermann Rodrigues (J. Braz. Comput. Soc., 2003)

Practical Type Inference for Polymorphic Recursion: an Implementation in Haskell. - Cristiano D. Vasconcellos; Lucília Figueiredo; Carlos Camarão 001 (J. Univers. Comput. Sci., 2003)

Constraint-set satisfiability for overloading. - Carlos Camarão 001; Lucília Figueiredo; Cristiano D. Vasconcellos (PPDP, 2004)

Open and Closed Worlds for Overloading: a Definition and Support for Coexistence. - Carlos Camarão 001; Cristiano D. Vasconcellos; Lucília Figueiredo; João Nicola (J. Univers. Comput. Sci., 2007)

Ambiguity and context-dependent overloading. - Rodrigo Geraldo Ribeiro; Carlos Camarão 001 (J. Braz. Comput. Soc., 2013)

Terminating constraint set satisfiability and simplification algorithms for context-dependent overloading. - Rodrigo Geraldo Ribeiro; Carlos Camarão 001; Lucília Figueiredo (J. Braz. Comput. Soc., 2013)

Mechanized metatheory for a λ-calculus with trust types. - Rodrigo Geraldo Ribeiro; Lucília Figueiredo; Carlos Camarão 001 (J. Braz. Comput. Soc., 2013)

Type Inference for GADTs and Anti-unification. - Adelaine Gelain; Cristiano D. Vasconcellos; Carlos Camarão 001; Rodrigo Geraldo Ribeiro (SBLP, 2015)

A Mechanized Textbook Proof of a Type Unification Algorithm. - Rodrigo Geraldo Ribeiro; Carlos Camarão 001 (SBMF, 2015)

Certified Derivative-Based Parsing of Regular Expressions. - Raul Lopes 002; Rodrigo Geraldo Ribeiro; Carlos Camarão 001 (SBLP, 2016)

Optional Type Classes for Haskell. - Rodrigo Geraldo Ribeiro; Carlos Camarão 001; Lucília Figueiredo; Cristiano D. Vasconcellos (SBLP, 2016)

Ambiguity and constrained polymorphism. - Carlos Camarão 001; Lucília Figueiredo; Rodrigo Geraldo Ribeiro (Sci. Comput. Program., 2016)

Special issue on revised and extended versions of papers presented at the 22nd Brazilian Symposium on Programming Languages (SBLP 2018). - Carlos Camarão 001; Martin Sulzmann (Sci. Comput. Program., 2022)