Burak Ekici

22 papers B 2C 1Journal 10Unranked 8
YearRankTypeTitle / Venue / Authors
2025 B conf
Formalising Subject Reduction and Progress for Multiparty Session Processes.
ITP
Burak Ekici, Tadayoshi Kamegai, Nobuko Yoshida
2024 B conf
Completeness of Asynchronous Session Tree Subtyping in Coq.
ITP
Burak Ekici, Nobuko Yoshida
2023 J jnl
A Sound Definitional Interpreter for a Simply Typed Functional Language.
Axioms
Burak Ekici
2023 — conf
Formal Verification of Bit-Vector Invertibility Conditions in Coq.
FroCoS
Burak Ekici, Arjun Viswanathan, Yoni Zohar, Cesare Tinelli, Clark W. Barrett
2020 J jnl
Mac Lane's Comparison Theorem for the Kleisli Construction Formalized in Coq.
Math. Comput. Sci.
Burak Ekici, Cezary Kaliszyk
2019 — conf
Verifying Bit-vector Invertibility Conditions in Coq (Extended Abstract).
PxTP
Burak Ekici, Arjun Viswanathan, Yoni Zohar, Clark W. Barrett, Cesare Tinelli
2018 C conf
Concrete Semantics with Coq and CoqHammer.
CICM
Lukasz Czajka, Burak Ekici, Cezary Kaliszyk
2018 J jnl
Concrete Semantics with Coq and CoqHammer.
CoRR
Lukasz Czajka, Burak Ekici, Cezary Kaliszyk
2018 J jnl
IMP with exceptions over decorated logic.
Discret. Math. Theor. Comput. Sci.
Burak Ekici
2018 — conf
Towards Mac Lane's Comparison Theorem for the (co)Kleisli Construction in Coq.
CICM Workshops
Burak Ekici
2017 — conf
SMTCoq: A Plug-In for Integrating SMT Solvers into Coq.
CAV (2)
Burak Ekici, Alain Mebsout, Cesare Tinelli, Chantal Keller, Guy Katz, Andrew Reynolds, Clark W. Barrett
2016 — conf
Extending SMTCoq, a Certified Checker for SMT (Extended Abstract).
HaTT@IJCAR
Burak Ekici, Guy Katz, Chantal Keller, Alain Mebsout, Andrew J. Reynolds, Cesare Tinelli
2015 — —
Certifications of programs with computational effects. (Certification de programmes avec des effets calculatoires).
Burak Ekici
2015 J jnl
Hilbert-Post completeness for the state and the exception effects.
CoRR
Jean-Guillaume Dumas, Dominique Duval, Burak Ekici, Damien Pous, Jean-Claude Reynaud
2015 J jnl
IMP with exceptions over decorated logic.
CoRR
Burak Ekici
2015 — conf
Relative Hilbert-Post Completeness for Exceptions.
MACIS
Jean-Guillaume Dumas, Dominique Duval, Burak Ekici, Damien Pous, Jean-Claude Reynaud
2014 J jnl
Certification of programs with computational effects.
CoRR
Burak Ekici
2014 — conf
Certified Proofs in Programs Involving Exceptions.
CICM Workshops
Jean-Guillaume Dumas, Dominique Duval, Burak Ekici, Jean-Claude Reynaud
2014 — conf
Formal verification in Coq of program properties involving the global state effect.
JFLA
Jean-Guillaume Dumas, Dominique Duval, Burak Ekici, Damien Pous
2014 J jnl
Procedural and Non-Procedural Implementation of Search Strategies in Control Network Programming.
CoRR
Kostadin Kratchanov, Emilia Golemanova, Tzanko Golemanov, Tuncay Ercan, Burak Ekici
2014 J jnl
Program certification with computational effects.
CoRR
Jean-Guillaume Dumas, Dominique Duval, Burak Ekici, Damien Pous
2013 J jnl
Formal verification in Coq of program properties involving the global state effect.
CoRR
Jean-Guillaume Dumas, Dominique Duval, Burak Ekici, Damien Pous