This page is a informal summary of my publications and the research projects I’ve been involed in.
Publications
Victor Cacciari Miraldo, Harold Carr, Mark Moir, Lisandra Silva and Guy L. Steele Jr. Formal Verification of Authenticated, Append-Only, Skip Lists in Agda, In CPP 2021, Virtual. pdf
Victor Cacciari Miraldo and Wouter Swierstra, An Efficient Algorithm for Type-Safe Structural Diffing, In ICFP 2019, Berlin. pdf
Alejandro Serrano Mena and Victor Cacciari Miraldo, Classes of Arbitrary Kind, In PADL 2019, Lisbon. pdf
Victor Cacciari Miraldo, Harold Carr, Alex Kogan, Mark Moir, Maurice Herlihy, Authenticated Modular Maps in Haskell, In TyDe 2018, St. Louis. slides
Alejandro Serrano Mena and Victor Cacciari Miraldo, Generic Programming of All Kinds, In Haskell Symposyum 2018, St. Louis. pdf slides
Victor Cacciari Miraldo and Alejandro Serrano Mena, Sums of Products for Mutually Recursive Datatypes, In TyDe 2018, St. Louis. pdf slides
Victor Cacciari Miraldo, Pierre-Évariste Dagand and Wouter Swierstra, Type-Directed Diffing of Structured Data, In TyDe 2017, Oxford. pdf
José Nuno Oliveira, Victor Cacciari Miraldo, “Keep definition, change category” — A practical approach to state-based system calculi, Journal of Logical and Algebraic Methods in Programming, 2015. link (Elsevier)
Victor C. Miraldo. Relational Equality in the Intensional Theory of Types. In Student-track, RAMiCS 2015, Braga, Portugal, 2015. pdf
Victor C. Miraldo, Cláudio B. Lourenço, Jorge S. Pinto, and Maria João Frade. Experimenting with predicate abstraction. In INFórum, Évora, Portugal, 2013. pdf
Cláudio B. Lourenço, Victor C. Miraldo, Jorge S. Pinto and Maria João Frade. SPARK-BMC: Checking SPARK code for bugs. In INFórum, Évora, Portugal, 2013.
Technical Reports
- Victor Cacciari Miraldo and Wouter Swierstra, Structure Aware Version Control: A generic approach using Agda. University of Utrecht. pdf
Research
2017 - 2020
Continuation and conclusion of my PhD at Utrecht University. I defended my PhD thesis (pdf) in October 2020.
Part-time employee of Oracle Labs, continuing the work performed during my internship.
2017 - 2017
- Internship at Oracle Labs Burlington, where I worked in the Scalable Synchronization Group (SSRG) under the supervision of Mark Moir. We conducted research in the blockchain area.
2015 - 2017
- PhD Candidate at Utrecht University, Software-Technology group, under the supervision of Wouter Swierstra. Paused the PhD for an internship.
2014 - 2015
- MSc dissertation. My Master’s dissertation is a combination of different topics. On one side we wanted to explore some form of proof automation in Agda, from where the by tactic was born. On the other hand, we wanted to use such tactic to provide a better equational reasoning framework for Relational Algebra. pdf
2013 - 2014
- Research Grant on QAIS Project. University of Minho, Braga, Portugal. Supervised by Professor José Nuno Oliveira. During this grant we investigated a calculus for probabilistic systems. The punchline is to use what we already have for functional programming and lift it to Mat, the Category of Matrices and Matrix Multiplication while modelling components as Monadic Mealy Machines, over the sub-distribution monad.
2012 - 2013
- Research Grant on AVIACC Project. University of Minho, Braga, Portugal. Supervised by Professors Jorge Sousa Pinto and Maria João Frade. This project was a mix of theory and practice. One objective was to understand the abstraction algorithms used in two industrial-strength Software Model Checkers. Namelly SLAM and SATABS. We found out that cartesian abstraction and the direct method are closer than we believed. Whereas another objective was to develop a software model checker for Spark, a subset of Ada. This development was integrated in a bigger effort, to also develop a bounded model checker for the language.
2011 - 2012
- Integration into Research Grant on “Interpretations of the lambda-calculus on interaction nets.” University of Minho, Braga, Portugal. Supervised by Professors José Carlos Espírito Santo and Jorge Sousa Pinto. This was my first contact with research. We studied how one could implement the lambda-calculus with a call-by-value evaluation semantics into interaction nets, which is a formalism very suitable for parallel computations. The process goes through translating a term to its equivalent logical proposition, encoding it in linear logic, going for it’s proof net representation and, finally, translating to a specific set of interaction nets. pdf (Portuguese)
Education
2018 - 2019
- Estonian Winter School in Computer Science, Palmse, ES.
2017 - 2018
- Computer-aided Security Proofs Fall-school, University of Aarhus, DK.
- Summer Internship at Oracle Labs, Burlingon MA, USA.
2016 - 2017
- Midlands Graduate School Summer School, University of Birmingham, UK.
2015 - 2016
- Enroled as a PhD candidate at University of Utrecht, the Netherlands.
2014 - 2015
2013 - 2014
- Partial time MSc Student. University of Minho, Braga, Portugal. Cryptography and Information Security
- Cyber-Physical Systems Spring School, by Professor André Platzer, CMU. University of Minho, Braga, Portugal.
2012 - 2013
- Partial time MSc Student. University of Minho, Braga, Portugal. Formal Methods in Software Engineering
- Advanced Functional Programming Summer School, University of Utrecht, Netherlands.
2009 - 2012
- Bachelor Student. University of Minho, Braga, Portugal. Computer Science. Graduated with ECTS scale A.