Coupled Schema Transformation and Data Conversion for XML and SQL. - Pablo Berdaguer; Alcino Cunha; Hugo Pacheco 001; Joost Visser 001 (PADL, 2007)

Algebraic Specialization of Generic Functions for Recursive Types. - Alcino Cunha; Hugo Pacheco 001 (MSFP@ICALP, 2008)

Mapping between Alloy Specifications and Database Implementations. - Alcino Cunha; Hugo Pacheco 001 (SEFM, 2009)

Generic Point-free Lenses. - Hugo Pacheco 001; Alcino Cunha (MPC, 2010)

Calculating with lenses: optimising bidirectional transformations. - Hugo Pacheco 001; Alcino Cunha (PEPM, 2011)

Relations as Executable Specifications: Taming Partiality and Non-determinism Using Invariants. - Nuno Macedo 001; Hugo Pacheco 001; Alcino Cunha (RAMiCS, 2012)

Bidirectional Transformation of Model-Driven Spreadsheets. - Jácome Cunha; João Paulo Fernandes; Jorge Mendes 001; Hugo Pacheco 001; João Saraiva (ICMT@TOOLS, 2012)

Multifocal: A Strategic Bidirectional Transformation Language for XML Schemas. - Hugo Pacheco 001; Alcino Cunha (ICMT@TOOLS, 2012)

Delta Lenses over Inductive Types. - Hugo Pacheco 001; Alcino Cunha; Zhenjiang Hu (Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 2012)

Bidirectional data transformation by calculation - Hugo Pacheco 001 (2012)

A Generic Scheme and Properties of Bidirectional Transformations. - Hugo Pacheco 001; Nuno Macedo 001; Alcino Cunha; Janis Voigtländer (CoRR, 2013)

Composing Least-change Lenses. - Nuno Macedo 001; Hugo Pacheco 001; Alcino Cunha; José Nuno Oliveira (Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 2013)

Towards a Framework for Multidirectional Model Transformations. - Nuno Macedo 001; Alcino Cunha; Hugo Pacheco 001 (EDBT/ICDT Workshops, 2014)

Validity Checking of Putback Transformations in Bidirectional Programming. - Zhenjiang Hu; Hugo Pacheco 001; Sebastian Fischer 001 (FM, 2014)

Writing bidirectional model transformations as intentional updates. - Tao Zan; Hugo Pacheco 001; Zhenjiang Hu (ICSE Companion, 2014)

Monadic combinators for "Putback" style bidirectional programming. - Hugo Pacheco 001; Zhenjiang Hu; Sebastian Fischer 001 (PEPM, 2014)

BiFluX: A Bidirectional Functional Update Language for XML. - Hugo Pacheco 001; Tao Zan; Zhenjiang Hu (PPDP, 2014)

Bidirectional spreadsheet formulas. - Nuno Macedo 001; Hugo Pacheco 001; Nuno Rocha Sousa; Alcino Cunha (VL/HCC, 2014)

A Clear Picture of Lens Laws - Functional Pearl. - Sebastian Fischer 001; Zhenjiang Hu; Hugo Pacheco 001 (MPC, 2015)

The essence of bidirectional programming. - Sebastian Fischer 001; Zhenjiang Hu; Hugo Pacheco 001 (Sci. China Inf. Sci., 2015)

A Tool-Chain for High-Assurance Cryptographic Software. - José Bacelar Almeida; Manuel Barbosa; Hugo Pacheco 001; Vitor Pereira 002 (ERCIM News, 2016)

Jasmin: High-Assurance and High-Speed Cryptography. - José Bacelar Almeida; Manuel Barbosa; Gilles Barthe; Arthur Blot; Benjamin Grégoire; Vincent Laporte; Tiago Oliveira 004; Hugo Pacheco 001; Benedikt Schmidt; Pierre-Yves Strub (CCS, 2017)

BiFluX: A Bidirectional Functional Update Language for XML. - Tao Zan; Hugo Pacheco 001; Hsiang-Shang Ko; Zhenjiang Hu (Inf. Media Technol., 2017)

Enforcing ideal-world leakage bounds in real-world secret sharing MPC frameworks. - José Bacelar Almeida; Manuel Barbosa; Gilles Barthe; Hugo Pacheco 001; Vitor Pereira 002; Bernardo Portela (IACR Cryptol. ePrint Arch., 2018)

Teaching how to program using automated assessment and functional glossy games (experience report). - José Bacelar Almeida; Alcino Cunha; Nuno Macedo 001; Hugo Pacheco 001; José Proença (Proc. ACM Program. Lang., 2018)

ROSY: An elegant language to teach the pure reactive nature of robot programming. - Hugo Pacheco 001; Nuno Macedo 001 (IRC, 2020)

Machine-checked ZKP for NP-relations: Formally Verified Security Proofs and Implementations of MPC-in-the-Head. - José Carlos Bacelar Almeida; Manuel Barbosa; Karim Eldefrawy; Stéphane Graham-Lengrand; Hugo Pacheco 001; Vitor Pereira 002 (CoRR, 2021)

Machine-checked ZKP for NP-relations: Formally Verified Security Proofs and Implementations of MPC-in-the-Head. - José Bacelar Almeida; Manuel Barbosa; Manuel L. Correia; Karim Eldefrawy; Stéphane Graham-Lengrand; Hugo Pacheco 001; Vitor Pereira 002 (IACR Cryptol. ePrint Arch., 2021)

A formal treatment of the role of verified compilers in secure computation. - José Carlos Bacelar Almeida; Manuel Barbosa; Gilles Barthe; Hugo Pacheco 001; Vitor Pereira 002; Bernardo Portela (J. Log. Algebraic Methods Program., 2022)

Formally verifying Kyber Part I: Implementation Correctness. - José Bacelar Almeida; Manuel Barbosa; Gilles Barthe; Benjamin Grégoire; Vincent Laporte; Jean-Christophe Léchenet; Tiago Oliveira 004; Hugo Pacheco 001; Miguel Quaresma; Peter Schwabe; Antoine Séré; Pierre-Yves Strub (IACR Cryptol. ePrint Arch., 2023)

General-Purpose Secure Conflict-free Replicated Data Types. - Bernardo Portela; Hugo Pacheco 001; Pedro Jorge; Rogério Pontes (IACR Cryptol. ePrint Arch., 2023)

Formally verifying Kyber Episode IV: Implementation correctness. - José Bacelar Almeida; Manuel Barbosa; Gilles Barthe; Benjamin Grégoire; Vincent Laporte; Jean-Christophe Léchenet; Tiago Oliveira 004; Hugo Pacheco 001; Miguel Quaresma; Peter Schwabe; Antoine Séré; Pierre-Yves Strub (IACR Trans. Cryptogr. Hardw. Embed. Syst., 2023)

Formally verifying Kyber Episode V: Machine-checked IND-CCA security and correctness of ML-KEM in EasyCrypt. - José Bacelar Almeida; Santiago Arranz-Olmos; Manuel Barbosa; Gilles Barthe; François Dupressoir; Benjamin Grégoire; Vincent Laporte; Jean-Christophe Léchenet; Cameron Low; Tiago Oliveira 004; Hugo Pacheco 001; Miguel Quaresma; et al. (IACR Cryptol. ePrint Arch., 2024)

Faster Verification of Faster Implementations: Combining Deductive and Circuit-Based Reasoning in EasyCrypt. - José Bacelar Almeida; Gustavo Xavier Delerue Marinho Alves; Manuel Barbosa; Gilles Barthe; Luís Esquível; Vincent Hwang; Tiago Oliveira 004; Hugo Pacheco 001; Peter Schwabe; Pierre-Yves Strub (SP, 2025)

oCANada: A Generation-Based Fuzzer for ECUs over CAN. - Thales Santos; Patrick Grümer; Reza Parsamehr; Hugo Pacheco 001 (VNC, 2025)