Maria João Frade

J. Log. Algebraic Methods Program., June, 2023

Variations and interpretations of naturality in call-by-name lambda-calculi with generalized applications.

[BibT_eX]

[DOI]

José Espírito Santo

Luís Pinto

J. Log. Algebraic Methods Program., February, 2023

2019

A generalized program verification workflow based on loop elimination and SA form.

[BibT_eX]

[DOI]

Proceedings of the 7th International Workshop on Formal Methods in Software Engineering, 2019

2018

A Generalized Approach to Verification Condition Generation.

[BibT_eX]

[DOI]

Shin Nakajima

Proceedings of the 2018 IEEE 42nd Annual Computer Software and Applications Conference, 2018

2016

A Single-Assignment Translation for Annotated Programs.

[BibT_eX]

[DOI]

CoRR, 2016

Permutability in Proof Terms for Intuitionistic Sequent Calculus with Cuts.

[BibT_eX]

[DOI]

José Espírito Santo

Luís Pinto

Proceedings of the 22nd International Conference on Types for Proofs and Programs, 2016

Formalizing Single-Assignment Program Verification: An Adaptation-Complete Approach.

[BibT_eX]

[DOI]

Proceedings of the Programming Languages and Systems, 2016

2014

A Bounded Model Checker for SPARK Programs.

[BibT_eX]

[DOI]

Proceedings of the Automated Technology for Verification and Analysis, 2014

2012

Verification conditions for single-assignment programs.

[BibT_eX]

[DOI]

Daniela Carneiro da Cruz

Proceedings of the ACM Symposium on Applied Computing, 2012

2011

Rigorous Software Development - An Introduction to Program Verification.

[BibT_eX]

[DOI]

Undergraduate Topics in Computer Science, Springer, ISBN: 978-0-85729-018-2, 2011

Verification conditions for source-level imperative programs.

[BibT_eX]

[DOI]

Comput. Sci. Rev., 2011

2009

Bidirectional data-flow analyses, type-systematically.

[BibT_eX]

[DOI]

Ando Saabas

Tarmo Uustalu

Proceedings of the 2009 ACM SIGPLAN Symposium on Partial Evaluation and Semantics-based Program Manipulation, 2009

2007

Foundational certification of data-flow analyses.

[BibT_eX]

[DOI]

Ando Saabas

Tarmo Uustalu

Proceedings of the First Joint IEEE/IFIP Symposium on Theoretical Aspects of Software Engineering, 2007

2006

Structural Proof Theory as Rewriting.

[BibT_eX]

[DOI]

José Espírito Santo

Luís Pinto

Proceedings of the Term Rewriting and Applications, 17th International Conference, 2006

2004

Type-based termination of recursive definitions.

[BibT_eX]

[DOI]

Math. Struct. Comput. Sci., 2004

2003

Type-based termination of recursive definitions and constructor subtyping in typed lambda calculi

[BibT_eX]

[DOI]

PhD thesis, 2003

1999

Constructor Subtyping.

[BibT_eX]

[DOI]

Gilles Barthe