Beta Ziliani
Beta Ziliani
FAMAF, UNC and CONICET
Verified email at mpi-sws.org - Homepage
Title
Cited by
Cited by
Year
Mtac: A monad for typed tactic programming in Coq
D DREYER, NR KRISHNASWAMI, A NANEVSKI, V VAFEIADIS
Journal of functional programming 25, 2015
792015
How to make ad hoc proof automation less ad hoc
G Gonthier, B Ziliani, A Nanevski, D Dreyer
ACM SIGPLAN Notices 46 (9), 163-175, 2011
612011
Lightweight proof by reflection using a posteriori simulation of effectful computation
G Claret, LCG Huesca, Y Régis-Gianas, B Ziliani
International Conference on Interactive Theorem Proving, 67-83, 2013
272013
How to make ad hoc proof automation less ad hoc
G Gonthier, A NANEVSKI, D DREYER
Journal of Functional Programming 23 (4), 357-401, 2013
252013
A unification algorithm for Coq featuring universe polymorphism and overloading
B Ziliani, M Sozeau
Proceedings of the 20th ACM SIGPLAN International Conference on Functional …, 2015
242015
Mtac2: typed tactics for backward reasoning in Coq
JO Kaiser, B Ziliani, R Krebbers, Y Régis-Gianas, D Dreyer
Proceedings of the ACM on Programming Languages 2 (ICFP), 1-31, 2018
212018
A comprehensible guide to a new unifier for CIC including universe polymorphism and overloading
M SOZEAU
Journal of Functional Programming 27, 2017
102017
Decoding lua: Formal semantics for the developer and the semanticist
M Soldevila, B Ziliani, B Silvestre, D Fridlender, F Mascarenhas
Proceedings of the 13th ACM SIGPLAN International Symposium on on Dynamic …, 2017
92017
Swapping: a natural bridge between named and indexed explicit substitution calculi
A Mendelzon, A Ríos, B Ziliani
arXiv preprint arXiv:1102.3730, 2011
32011
Mechanizing Bisimulation Theorems for Relation-Changing Logics in Coq
R Fervari, F Trucco, B Ziliani
International Workshop on Dynamic Logic, 3-18, 2019
22019
Towards a better-behaved unification algorithm for Coq
B Ziliani, M Sozeau
RISC-Linz, 74, 2014
12014
Verification of dynamic bisimulation theorems in Coq
R Fervari, F Trucco, B Ziliani
Journal of Logical and Algebraic Methods in Programming 120, 100642, 2021
2021
Understanding Lua’s Garbage Collection: Towards a Formalized Static Analyzer
M Soldevila, B Ziliani, D Fridlender
Proceedings of the 22nd International Symposium on Principles and Practice …, 2020
2020
Understanding Lua’s Garbage Collection
M Soldevila, B Ziliani, D Fridlender
2020
The Next 700 Safe Tactic Languages
B Ziliani, Y Régis-Gianas, JO Kaiser
Submitted for publication, 2016
2016
Interactive typed tactic programming in the coq proof assistant
B Ziliani
2015
Generalization of Meta-Programs with Dependent Types in Mtac2 with Mtac2
I Tiraboschi, JO Kaiser, B Ziliani
Introducing MetaCoq: A Safe Tactic Language for Coq
B Ziliani
The system can't perform the operation now. Try again later.
Articles 1–18