"Keep definition, change category" - A practical approach to state-based system calculi. - José Nuno Oliveira; Victor Cacciari Miraldo (J. Log. Algebraic Methods Program., 2016)

Type-directed diffing of structured data. - Victor Cacciari Miraldo; Pierre-Évariste Dagand; Wouter Swierstra (TyDe@ICFP, 2017)

Generic programming of all kinds. - Alejandro Serrano 001; Victor Cacciari Miraldo (Haskell@ICFP, 2018)

Authenticated modular maps in Haskell. - Victor Cacciari Miraldo; Harold Carr; Alex Kogan; Mark Moir; Maurice Herlihy (TyDe@ICFP, 2018)

Sums of products for mutually recursive datatypes: the appropriationist's view on generic programming. - Victor Cacciari Miraldo; Alejandro Serrano 001 (TyDe@ICFP, 2018)

Classes of Arbitrary Kind. - Alejandro Serrano 001; Victor Cacciari Miraldo (PADL, 2019)

An efficient algorithm for type-safe structural diffing. - Victor Cacciari Miraldo; Wouter Swierstra (Proc. ACM Program. Lang., 2019)

Formal verification of authenticated, append-only skip lists in Agda. - Victor Cacciari Miraldo; Harold Carr; Mark Moir; Lisandra Silva; Guy L. Steele Jr. (CPP, 2021)

Formal Verification of Authenticated, Append-Only Skip Lists in Agda: Extended Version. - Victor Cacciari Miraldo; Harold Carr; Mark Moir; Lisandra Silva; Guy L. Steele Jr. (CoRR, 2021)

Towards Formal Verification of HotStuff-Based Byzantine Fault Tolerant Consensus in Agda. - Harold Carr; Christa Jenkins; Mark Moir; Victor Cacciari Miraldo; Lisandra Silva (NFM, 2022)

Towards Formal Verification of HotStuff-based Byzantine Fault Tolerant Consensus in Agda: Extended Version. - Harold Carr; Christopher Jenkins; Mark Moir; Victor Cacciari Miraldo; Lisandra Silva (CoRR, 2022)

An approach to translating Haskell programs to Agda and reasoning about them. - Harold Carr; Christa Jenkins; Mark Moir; Victor Cacciari Miraldo; Lisandra Silva (CoRR, 2022)