Andrea Condoluci

PhD in Computer Science & Logic

A picture of Andrea's face

I am a software engineer at Tweag I/O and a researcher on the theory of programming languages. My main interests are interpreters, optimising compilers, certified programming, and formal methods in general. I spend most of my days doing functional programming. At night, I dream about the nature of computation, and how to decentralize and democratize internet services.

🏃‍♀️ Currently

Software Engineer

2019 - ⏱
Tweag I/O Software Innovation Lab
  • Investigating incremental garbage collection in Asterius, the Haskell-to-Wasm compiler
  • Writing type-level Haskell web services with focus on concurrency, availability, and data integrity
  • Rapid iteration & Continuous Integration

🎓 Education

PhD in Computer Science

2016 - 2019
Alma Mater Studiorum - Università di Bologna
Researched how to check if two programs are equivalent in an efficient way.
My focus was on the λ-calculus (the formal theory behind functional programming languages) where the notion of equivalence is β-convertibility of terms. I applied different techniques (graphs, abstract machines) to show that conversion can be decided in time linear in the number of reduction steps.
📕 Dissertation: β-conversion, efficiently

European MSc in Computational Logic

2014 - 2016
Technische Universität Dresden, Free University of Bozen - Bolzano, Technische Universität Wien
  • Attended EMCL, a distributed two-year master’s program in the field of Computational Logic (see
  • Co-organized the “EMCL 2016 Workshop”​ in Vienna, a two-days workshop with talks by EMCL students, alumni and professors.
📕 Dissertation: Cut-elimination by Resolution and Propositional Proof Schemata

Electronic Music

2013 - 2014

BSc in Mathematics

2009 - 2013
Università degli Studi di Padova
Type Theory · Mathematical Logic · Foundation of Mathematics

🌴 Internships

INRIA, 🇫🇷 Paris Saclay

Parsifal Team
Strengthened my knowledge on abstract machines, a first-order formalism to study evaluations of programs in the λ-calculus, also from the point of view of efficiency.

Data61, 🇦🇺 Canberra

Aug - Oct 2015
Software Systems Group
Wrote a library to define co-inductive datatypes in the HOL proof assistant

👩‍🚀 Work Experience

Teaching Assistant

  • Programming (marked midterms)
  • Algorithms & Data structures (lead a weekly three-hour tutorial)
  • Mathematical Logic (co-lead weekly tutorial & marked midterms)

    Freelance Frontend Developer

    Developed Open Sheet Music Display, an open source Typescript library to render MusicXML scores in the browser. See

      📖 Publications

      Strong Call-by-Value is Reasonable, Implosively

      Beniamino Accattoli, Andrea Condoluci and Claudio Sacerdoti Coen
      LICS 2021 (29 June – 02 July, 2021, Virtual)

      Sharing Equality is Linear

      Andrea Condoluci, Beniamino Accattoli and Claudio Sacerdoti Coen
      PPDP 2019 (October, 7, 2019 Porto, Portugal)

      Crumbling Abstract Machines

      Beniamino Accattoli, Andrea Condoluci, Giulio Guerrieri and Claudio Sacerdoti Coen
      PPDP 2019 (October, 7, 2019 Porto, Portugal)

      Admissible Tools in the Kitchen of Intuitionistic Logic

      Andrea Condoluci and Matteo Manighetti
      CL&C 2018 (July, 7, 2018 Oxford, UK)

      Relational Data Across Mathematical Libraries

      Andrea Condoluci, Michael Kohlhase, Dennis Müller, Florian Rabe, Claudio Sacerdoti Coen, and Makarius Wenzel
      CICM 2019 (July 8-12, 2019 Prague, Czech Republic)