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, breath and live
• Praud cat dad x 2
• Got a PhD

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

I am currently working on the application of formal methods, mainly runtime verification, different technologies in collaboration with Prof. César Sánchez. One of the applications is blockchains where we are trying to characterize the interaction between smart contract and new strategies to scale blockchains, the so called layer 2 schemes.

We are also developing a non-turing complete language for embedded systems. Designing embedded systems for critical system (satellites in this case) is hard and a very studied problem. Our proposal is to design a simple language, close to the current state of affairs, and verify small parts of it. Stay tuned, we are about to publish it :D.

• 2022 - Multi: A Formal Playground for Multi-Smart Contract Interaction
• 2022 - Setchain: Improving Blockchain Scalability with Byzantine Distributed Sets and Barriers
• 2022 - Transaction Monitoring of Smart Contracts
• 2022 - Effectful improvement theory
• 2020 - Declarative Stream Runtime Verification (hLola)

During the end of 2020 and beginning of 2021, I did a internship at IMDEA Software Institute collaborating with Prof. César Sánchez. We studied the behaviour emerging from the interaction between smart contracts and how to formally specify and verify properties about smart contracts. We developed a Coq library called Multi to study the behaviour emerging from the interaction between smart-contracts. Happily, we did not conclude our work and I am still working with César.

I did my PhD research 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 of my thesis was to develop an effectful improvement theory, i.e. an improvement theory for languages with algebraic effects.

In collaboration with Gustavo Grieco, Pablo Buiras andAgustin Mista, we developed random generation test case tool based on Haskell complex types, QuickCheck and how implementors define complex data structures in their libraries. My main contribution was to extend the initial code base developed by Pablo, and designing new strategies to automatic derive QuickCheck arbitrary classes, resulting a tool we called MegaDeTH . The tool is called QuickFuzz, but sadly is not maintain anymore.

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

In 2013, I did an intership 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.