Beta Ziliani

According to our database, Beta Ziliani authored at least 17 papers between 2010 and 2024.

Collaborative distances:

• Dijkstra number of three.
• Erdős number of four.

2024

redex2coq.

Mallku Soldevila, Rodrigo Geraldo Ribeiro, Beta Ziliani

Dataset, November, 2024

Redex -> Coq: towards a theory of decidability of Redex's reduction semantics.

Mallku Soldevila, Rodrigo Geraldo Ribeiro, Beta Ziliani

CoRR, 2024

Redex2Coq: Towards a Theory of Decidability of Redex's Reduction Semantics.

Mallku Soldevila, Rodrigo Geraldo Ribeiro, Beta Ziliani

Proceedings of the 15th International Conference on Interactive Theorem Proving, 2024

2022

From Specification to Testing: Semantics Engineering for Lua 5.2.

Mallku Soldevila, Beta Ziliani, Bruno Silvestre

J. Autom. Reason., 2022

2021

Verification of dynamic bisimulation theorems in Coq.

Raul Fervari, Francisco Trucco, Beta Ziliani

J. Log. Algebraic Methods Program., 2021

2020

Understanding Lua's Garbage Collection: Towards a Formalized Static Analyzer.

Mallku Soldevila, Beta Ziliani, Daniel Fridlender

Proceedings of the PPDP '20: 22nd International Symposium on Principles and Practice of Declarative Programming, 2020

2019

Mechanizing Bisimulation Theorems for Relation-Changing Logics in Coq.

Raul Fervari, Francisco Trucco, Beta Ziliani

Proceedings of the Dynamic Logic. New Trends and Applications, 2019

2018

Mtac2: typed tactics for backward reasoning in Coq.

Jan-Oliver Kaiser, Beta Ziliani, Robbert Krebbers, Yann Régis-Gianas, Derek Dreyer

Proc. ACM Program. Lang., 2018

2017

A comprehensible guide to a new unifier for CIC including universe polymorphism and overloading.

Beta Ziliani, Matthieu Sozeau

J. Funct. Program., 2017

Decoding Lua: formal semantics for the developer and the semanticist.

Mallku Soldevila, Beta Ziliani, Bruno Silvestre, Daniel Fridlender, Fabio Mascarenhas

Proceedings of the 13th ACM SIGPLAN International Symposium on on Dynamic Languages, Vancouver, BC, Canada, October 23, 2017

2015

Interactive typed tactic programming in the Coq proof assistant.

Beta Ziliani

PhD thesis, 2015

Mtac: A monad for typed tactic programming in Coq.

Beta Ziliani, Derek Dreyer, Neelakantan R. Krishnaswami, Aleksandar Nanevski, Viktor Vafeiadis

J. Funct. Program., 2015

A unification algorithm for Coq featuring universe polymorphism and overloading.

Beta Ziliani, Matthieu Sozeau

Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming, 2015

2014

Towards a better-behaved unification algorithm for Coq.

Beta Ziliani, Matthieu Sozeau

Proceedings of the 28th International Workshop on Unification, 2014

2013

How to make ad hoc proof automation less ad hoc.

Georges Gonthier, Beta Ziliani, Aleksandar Nanevski, Derek Dreyer

J. Funct. Program., 2013

Lightweight Proof by Reflection Using a Posteriori Simulation of Effectful Computation.

Guillaume Claret, Lourdes Del Carmen González-Huesca, Yann Régis-Gianas, Beta Ziliani

Proceedings of the Interactive Theorem Proving - 4th International Conference, 2013

2010

Swapping: a natural bridge between named and indexed explicit substitution calculi

Ariel Mendelzon, Alejandro Ríos, Beta Ziliani

Proceedings of the Proceedings 5th International Workshop on Higher-Order Rewriting, 2010