Beta Ziliani

20 papers A 3B 2C 2Journal 9Unranked 3
YearRankTypeTitle / Venue / Authors
2024 J jnl
Redex -> Coq: towards a theory of decidability of Redex's reduction semantics.
CoRR
Mallku Soldevila, Rodrigo Geraldo Ribeiro, Beta Ziliani
2024 B conf
Redex2Coq: Towards a Theory of Decidability of Redex's Reduction Semantics.
ITP
Mallku Soldevila, Rodrigo Geraldo Ribeiro, Beta Ziliani
2022 J jnl
From Specification to Testing: Semantics Engineering for Lua 5.2.
J. Autom. Reason.
Mallku Soldevila, Beta Ziliani, Bruno Silvestre
2021 J jnl
Verification of dynamic bisimulation theorems in Coq.
J. Log. Algebraic Methods Program.
Raul Fervari, Francisco Trucco, Beta Ziliani
2020 J jnl
Understanding Lua's Garbage Collection - Towards a Formalized Static Analyzer.
CoRR
Mallku Soldevila, Beta Ziliani, Daniel Fridlender
2020 C conf
Understanding Lua's Garbage Collection: Towards a Formalized Static Analyzer.
PPDP
Mallku Soldevila, Beta Ziliani, Daniel Fridlender
2019 — conf
Mechanizing Bisimulation Theorems for Relation-Changing Logics in Coq.
DaLí
Raul Fervari, Francisco Trucco, Beta Ziliani
2018 J jnl
Mtac2: typed tactics for backward reasoning in Coq.
Proc. ACM Program. Lang.
Jan-Oliver Kaiser, Beta Ziliani, Robbert Krebbers, Yann Régis-Gianas, Derek Dreyer
2017 J jnl
A comprehensible guide to a new unifier for CIC including universe polymorphism and overloading.
J. Funct. Program.
Beta Ziliani, Matthieu Sozeau
2017 J jnl
Decoding Lua: Formal Semantics for the Developer and the Semanticist.
CoRR
Mallku Soldevila, Beta Ziliani, Bruno Silvestre, Daniel Fridlender, Fabio Mascarenhas
2017 C conf
Decoding Lua: formal semantics for the developer and the semanticist.
DLS
Mallku Soldevila, Beta Ziliani, Bruno Silvestre, Daniel Fridlender, Fabio Mascarenhas
2015 A conf
A unification algorithm for Coq featuring universe polymorphism and overloading.
ICFP
Beta Ziliani, Matthieu Sozeau
2015 — —
Interactive typed tactic programming in the Coq proof assistant.
Beta Ziliani
2015 J jnl
Mtac: A monad for typed tactic programming in Coq.
J. Funct. Program.
Beta Ziliani, Derek Dreyer, Neelakantan R. Krishnaswami, Aleksandar Nanevski, Viktor Vafeiadis
2014 — conf
Towards a better-behaved unification algorithm for Coq.
UNIF
Beta Ziliani, Matthieu Sozeau
2013 J jnl
How to make ad hoc proof automation less ad hoc.
J. Funct. Program.
Georges Gonthier, Beta Ziliani, Aleksandar Nanevski, Derek Dreyer
2013 B conf
Lightweight Proof by Reflection Using a Posteriori Simulation of Effectful Computation.
ITP
Guillaume Claret, Lourdes Del Carmen González-Huesca, Yann Régis-Gianas, Beta Ziliani
2013 A conf
Mtac: a monad for typed tactic programming in Coq.
ICFP
Beta Ziliani, Derek Dreyer, Neelakantan R. Krishnaswami, Aleksandar Nanevski, Viktor Vafeiadis
2011 A conf
How to make ad hoc proof automation less ad hoc.
ICFP
Georges Gonthier, Beta Ziliani, Aleksandar Nanevski, Derek Dreyer
2010 — conf
Swapping: a natural bridge between named and indexed explicit substitution calculi
HOR
Ariel Mendelzon, Alejandro Ríos, Beta Ziliani