Martín Ceresa Website!

martin.nope@ceresa.ar
web.martin.nope@ceresa.ar
martin.ceresa.nope@iohk.io

5BDFA36B5238CBD0

@martinceresa

About me

My name is Martín Ceresa and I am me.

I do several things and some represent me more than others:

  • Capoeira GCALV
  • Meditate, yoga, breathe and live
  • Happily sharing my life with Annie
  • Proud cat dad x 2
  • Got a PhD

Job Life

Currently a Formal Methods Engineer on the research team at IO-G.

Projects

  • [2025-05-12] Midgard : Formalization of L2 optimistic rollups for Cardano.
  • [2024-12-10] Lean Games : Mechanization of Fraud Proof Arbitration games in Lean4. Digital Twin of players.
  • [2022-03-10] Termina – Programming Language : Termina is a domain-specific language for real-time embedded systems aimed at simplifying their implementation and reducing validation and verification costs.

See more

Publications

Journals

  • “Setchain Algorithms for Blockchain Scalability.” Karmegam, Arivarasan, Gabina Luz Bianchi, Margarita Capretto, Martín Ceresa, Antonio Fernández Anta, and César Sánchez. https://doi.org/10.1016/J.TCS.2026.116145.
  • “A Decentralized Sequencer and Data Availability Committee for Rollups Using Set Consensus.” Capretto, Margarita, Martín Ceresa, Antonio Fernández Anta, Pedro Moreno-Sanchez, and César Sánchez. https://doi.org/10.48550/ARXIV.2503.05451.
  • “A Secure Sequencer and Data Availability Committee for Rollups (Extended Version).” Capretto, Margarita, Martín Ceresa, Antonio Fernández Anta, Pedro Moreno-Sanchez, and César Sánchez. https://doi.org/10.48550/ARXIV.2509.06614.

Complete List

Conferences

Complete List

Research Path

My interests include: computer science, programming languages, type theory, category theory, mathematics and its foundations, topology and logic. Recently, I have found myself studying the history and philosophy of mathematics.

I worked on formal methods, mainly runtime verification and related technologies, in collaboration with Prof. César Sánchez. One of the applications is blockchains, where we tried to characterise the interaction between smart contract and new strategies for scaling blockchains (L2-schemes).

I collaborated on the design and initial development of Termina, a non-Turing complete language for embedded systems. Designing embedded systems for critical system (satellites, in this case) is a hard old problem. Our proposal is to design a simple language, close to the current state of affairs, and verify small parts of it.

Between late 2020 and early 2021, I did an internship at IMDEA Software Institute collaborating with Prof. César Sánchez. We studied the computational emerging behaviour from the interaction between smart contracts, and how to formally specify and verify properties about them. The result was a Coq library called Multi.

I did my PhD in Argentina at CIFASIS under the guidance of Dr. Mauro Jaskelioff. My thesis focused on Improvement Theory, developed extensively by Prof. Sands early in the nineties. The main goal was to develop an effectful improvement theory, i.e. an improvement theory for languages with algebraic effects.

In collaboration with Gustavo Grieco, Pablo Buiras and Agustin Mista, we developed a random generation test case tool based on Haskell complex types, QuickCheck and how developers define complex data structures in their libraries, called QuickFuzz. I extended the initial code base developed by Pablo and designed new strategies to automatically derive QuickCheck `Arbitrary` instances, resulting in a tool we called MegaDeTH.

Until 2015, I was a student in the Department of Computer Science at Universidad Nacional de Rosario.

In 2013, I did an internship at IMDEA Software Institute (Madrid, Spain) under the supervision of Benedikt Schmidt, in the development of automatic tactics in EasyCrypt. In this internship, I learned about modern cryptography proofs, and a bit about tactic development. I developed an automatic tactic (or megatactic) which implemented a classic cryptography step called optimistic sampling.