Logo

Beta Ziliani

 beta.ziliani@gmail.com

Team Lead and Product Manager @ Manas.Tech. Past Associate Lecturer @ FAMAF, UNC.

Powered by Jekyll — Theme by BDHU

Research

I got my PhD with honors from the University of Saarland and Max Plank Institute for Software Systems, under the supervision of Dr. Derek Dreyer. Before that I got my licenciatura (~ MSc.) from FCEyN, UBA (Argentina).

Then I moved back to Argentina and got a researcher position at CONICET and FAMAF, UNC, and got promoted to the second stage (two after postdoc). But this is old story now: I’ve moved back to the industry. This said, I still have projects I’m trying to finish on my “spare time” (*laughs in parenting*).

Service Alumni Publications


Service


Alumni

PhD

  1. Soldevila Raffa, M. E. (2021). Semántica operacional y su aplicación para el estudio de recolección de basura, en Lua 5.2. FAMAF, UNC. (doi, open access)

Licenciatura (~ MSc.)

  1. Tiraboschi, I. (2020). Generalización de meta-programas con tipado dependiente en Mtac2. FAMAF, UNC. (doi, open access)
  2. Trucco, F. C. (2019). Verificación de lógicas modales dinámicas en Coq. FAMAF, UNC. (doi, open access)
  3. Mendelzon, A. (2010). Una curiosa versión de λdB basada en “swappings”: aplicación a traducciones entre cálculos de sustituciones explícitas con nombres e índices. FCEyN, UBA. (pdf)


Publications

Journals

  1. Soldevila, M., Ziliani, B., and Silvestre, B. (2022). From specification to testing: semantics engineering for Lua 5.2. Journal of Automated Reasoning, 66(905-952) . (doi, pdf)
  2. Fervari, R., Trucco, F., and Ziliani, B. (2021). Verification of dynamic bisimulation theorems in Coq. Journal of Logical and Algebraic Methods in Programming, 120(100642) . (doi, pdf)
  3. Kaiser, J.-O., Ziliani, B., Krebbers, R., Régis-Gianas, Y., and Dreyer, D. (2018). Mtac2: Typed Tactics for Backward Reasoning in Coq. Proc. ACM Program. Lang., 2(78:1–78:31) . (doi, open access)
  4. Ziliani, B. and Sozeau, M. (2017). A comprehensible guide to a new unifier for CIC including universe polymorphism and overloading. Journal of Functional Programming, 27 . (doi, open access)
  5. Ziliani, B., Dreyer, D., Krishnaswami, N. R., Nanevski, A., and Vafeiadis, V. (2015). Mtac: A monad for typed tactic programming in Coq. Journal of Functional Programming, 25 . (doi, open access)
  6. Gonthier, G., Ziliani, B., Nanevski, A., and Dreyer, D. (2013). How to make ad hoc proof automation less ad hoc. Journal of Functional Programming, 23(357–401) . (doi, open access)

Proceedings

These are all peer-reviewed, long papers.

  1. Soldevila, M., Ribeiro, R., and Ziliani, B. (2024). Redex2Coq: Towards a Theory of Decidability of Redex’s Reduction Semantics. Proceedings of the 15th International Conference on Interactive Theorem Proving (ITP 2024), 309(34:1–34:18) . (doi, open access)
  2. Soldevila, M., Ziliani, B., and Fridlender, D. (2020). Understanding Lua’s Garbage Collection: Towards a Formalized Static Analyzer. Proceedings of the 22nd International Symposium on Principles and Practice of Declarative Programming. (doi, open access)
  3. Fervari, R., Trucco, F., and Ziliani, B. (2019). Mechanizing Bisimulation Theorems for Relation-Changing Logics in Coq. Proceedings of the 2nd Workshop on Dynamic Logic: New Trends and Applications. (doi, pdf)
  4. Soldevila, M., Ziliani, B., Silvestre, B., Fridlender, D., and Mascarenhas, F. (2017). Decoding Lua: Formal Semantics for the Developer and the Semanticist. Proceedings of the 13th ACM SIGPLAN Dynamic Languages Symposium. (doi, pdf)
  5. Ziliani, B. and Sozeau, M. (2015). A Unification Algorithm for Coq Featuring Universe Polymorphism and Overloading. Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming. (doi, pdf)
  6. Ziliani, B., Dreyer, D., Krishnaswami, N. R., Nanevski, A., and Vafeiadis, V. (2013). Mtac: A Monad for Typed Tactic Programming in Coq. Proceedings of the 18th ACM SIGPLAN International Conference on Functional Programming. (doi, pdf)
  7. Claret, G., Carmen González Huesca, L., Régis-Gianas, Y., and Ziliani, B. (2013). Lightweight Proof by Reflection Using a Posteriori Simulation of Effectful Computation. Proceedings of the 4th International Conference on Theorem Proving. (doi, pdf)
  8. Gonthier, G., Ziliani, B., Nanevski, A., and Dreyer, D. (2011). How to Make Ad Hoc Proof Automation Less Ad Hoc. Proceedings of the 16th ACM SIGPLAN International Conference on Functional Programming. (doi, pdf)
  9. Mendelzon, A., Rı́os, A., and Ziliani, B. (2010). Swapping: a natural bridge between named and indexed explicit substitution calculi. Proceedings of the 5th international workshop on Higher-Order Rewriting. (doi, open access)

Theses

  1. Ziliani, B. (2015). Interactive Typed Tactic Programming for the Coq Proof Assistant. MPI-SWS and University of Saarland (UdS). (doi, open access)
  2. Ziliani, B. (2009). λσgc: Un cálculo basado en λσ con Garbage Collection. Universidad de Buenos Aires (UBA). (pdf)