Constructor Subtyping. - Gilles Barthe; Maria João Frade (ESOP, 1999)

Type-based termination of recursive definitions and constructor subtyping in typed lambda calculi - Maria João Frade (2003)

Type-based termination of recursive definitions. - Gilles Barthe; Maria João Frade; Eduardo Giménez 001; Luís Pinto 001; Tarmo Uustalu (Math. Struct. Comput. Sci., 2004)

Structural Proof Theory as Rewriting. - José Espírito Santo; Maria João Frade; Luís Pinto 001 (RTA, 2006)

Foundational certification of data-flow analyses. - Maria João Frade; Ando Saabas; Tarmo Uustalu (TASE, 2007)

Bidirectional data-flow analyses, type-systematically. - Maria João Frade; Ando Saabas; Tarmo Uustalu (PEPM, 2009)

Verification conditions for source-level imperative programs. - Maria João Frade; Jorge Sousa Pinto (Comput. Sci. Rev., 2011)

Rigorous Software Development - An Introduction to Program Verification. - José Bacelar Almeida; Maria João Frade; Jorge Sousa Pinto; Simão Melo de Sousa (Springer, 2011)

Verification conditions for single-assignment programs. - Daniela Carneiro da Cruz; Maria João Frade; Jorge Sousa Pinto (SAC, 2012)

A Bounded Model Checker for SPARK Programs. - Cláudio Belo Lourenço; Maria João Frade; Jorge Sousa Pinto (ATVA, 2014)

Formalizing Single-Assignment Program Verification: An Adaptation-Complete Approach. - Cláudio Belo Lourenço; Maria João Frade; Jorge Sousa Pinto (ESOP, 2016)

Permutability in Proof Terms for Intuitionistic Sequent Calculus with Cuts. - José Espírito Santo; Maria João Frade; Luís Pinto 001 (TYPES, 2016)

A Single-Assignment Translation for Annotated Programs. - Cláudio Belo Lourenço; Maria João Frade; Jorge Sousa Pinto (CoRR, 2016)

A Generalized Approach to Verification Condition Generation. - Cláudio Belo Lourenço; Maria João Frade; Shin Nakajima 001; Jorge Sousa Pinto (COMPSAC (1), 2018)

A generalized program verification workflow based on loop elimination and SA form. - Cláudio Belo Lourenço; Maria João Frade; Jorge Sousa Pinto (FormaliSE@ICSE, 2019)

Variations and interpretations of naturality in call-by-name lambda-calculi with generalized applications. - José Espírito Santo; Maria João Frade; Luís Pinto 001 (J. Log. Algebraic Methods Program., 2023)

A verified VCGen based on dynamic logic: An exercise in meta-verification with Why3. - Maria João Frade; Jorge Sousa Pinto (J. Log. Algebraic Methods Program., 2023)