Folgen
Beta Ziliani
Beta Ziliani
FAMAF, UNC and Manas.Tech
Bestätigte E-Mail-Adresse bei mpi-sws.org - Startseite
Titel
Zitiert von
Zitiert von
Jahr
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
672011
Mtac: a monad for typed tactic programming in Coq
B Ziliani, D Dreyer, NR Krishnaswami, A Nanevski, V Vafeiadis
ACM SIGPLAN Notices 48 (9), 87-100, 2013
562013
Mtac: A monad for typed tactic programming in Coq
B Ziliani, D Dreyer, NR Krishnaswami, A Nanevski, V Vafeiadis
Journal of functional programming 25, e12, 2015
472015
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
382018
How to make ad hoc proof automation less ad hoc
G Gonthier, B Ziliani, A Nanevski, D Dreyer
Journal of Functional Programming 23 (4), 357-401, 2013
362013
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
342015
Lightweight proof by reflection using a posteriori simulation of effectful computation
G Claret, L del Carmen González Huesca, Y Régis-Gianas, B Ziliani
Interactive Theorem Proving: 4th International Conference, ITP 2013, Rennes …, 2013
282013
A comprehensible guide to a new unifier for CIC including universe polymorphism and overloading
B Ziliani, M Sozeau
Journal of Functional Programming 27, e10, 2017
182017
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
152017
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
62020
Mechanizing bisimulation theorems for relation-changing logics in Coq
R Fervari, F Trucco, B Ziliani
Dynamic Logic. New Trends and Applications: Second International Workshop …, 2020
32020
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
From specification to testing: semantics engineering for Lua 5.2
M Soldevila, B Ziliani, B Silvestre
Journal of Automated Reasoning 66 (4), 905-952, 2022
22022
Verification of dynamic bisimulation theorems in Coq
R Fervari, F Trucco, B Ziliani
Journal of Logical and Algebraic Methods in Programming 120, 100642, 2021
22021
Towards a better-behaved unification algorithm for Coq.
B Ziliani, M Sozeau
UNIF, 74-87, 2014
12014
Redex-> Coq: towards a theory of decidability of Redex's reduction semantics
M Soldevila, R Ribeiro, B Ziliani
arXiv preprint arXiv:2402.03488, 2024
2024
redex2coq
M Soldevila, R Ribeiro, B Ziliani
Schloss Dagstuhl–Leibniz-Zentrum für Informatik, 2024
2024
Understanding Lua’s Garbage Collection
M Soldevila, B Ziliani, D Fridlender
2020
Decoding Lua: formal semantics for the developer and the semanticist
ME Soldevila Raffa, B Ziliani, B Silvestre, DE Fridlender, F Mascarenhas
Association for Computing Machinery, 2018
2018
Interactive typed tactic programming in the coq proof assistant
B Ziliani
2015
Das System kann den Vorgang jetzt nicht ausführen. Versuchen Sie es später erneut.
Artikel 1–20