Formal verification in Coq of program properties involving the global state effect. - Jean-Guillaume Dumas; Dominique Duval; Burak Ekici; Damien Pous (JFLA, 2014)

Certified Proofs in Programs Involving Exceptions. - Jean-Guillaume Dumas; Dominique Duval; Burak Ekici; Jean-Claude Reynaud (CICM Workshops, 2014)

Program certification with computational effects. - Jean-Guillaume Dumas; Dominique Duval; Burak Ekici; Damien Pous (CoRR, 2014)

Certification of programs with computational effects. - Burak Ekici (CoRR, 2014)

Procedural and Non-Procedural Implementation of Search Strategies in Control Network Programming. - Kostadin Kratchanov; Emilia Golemanova; Tzanko Golemanov; Tuncay Ercan; Burak Ekici (CoRR, 2014)

Relative Hilbert-Post Completeness for Exceptions. - Jean-Guillaume Dumas; Dominique Duval; Burak Ekici; Damien Pous; Jean-Claude Reynaud (MACIS, 2015)

Hilbert-Post completeness for the state and the exception effects. - Jean-Guillaume Dumas; Dominique Duval; Burak Ekici; Damien Pous; Jean-Claude Reynaud (CoRR, 2015)

Certifications of programs with computational effects. (Certification de programmes avec des effets calculatoires). - Burak Ekici (2015)

Extending SMTCoq, a Certified Checker for SMT (Extended Abstract). - Burak Ekici; Guy Katz; Chantal Keller; Alain Mebsout; Andrew J. Reynolds; Cesare Tinelli (HaTT@IJCAR, 2016)

SMTCoq: A Plug-In for Integrating SMT Solvers into Coq. - Burak Ekici; Alain Mebsout; Cesare Tinelli; Chantal Keller; Guy Katz; Andrew Reynolds 001; Clark W. Barrett (CAV (2), 2017)

Concrete Semantics with Coq and CoqHammer. - Lukasz Czajka 001; Burak Ekici; Cezary Kaliszyk (CICM, 2018)

Towards Mac Lane's Comparison Theorem for the (co)Kleisli Construction in Coq. - Burak Ekici (CICM Workshops, 2018)

IMP with exceptions over decorated logic. - Burak Ekici (Discret. Math. Theor. Comput. Sci., 2018)

Verifying Bit-vector Invertibility Conditions in Coq (Extended Abstract). - Burak Ekici; Arjun Viswanathan 001; Yoni Zohar; Clark W. Barrett; Cesare Tinelli (PxTP, 2019)

Mac Lane's Comparison Theorem for the Kleisli Construction Formalized in Coq. - Burak Ekici; Cezary Kaliszyk (Math. Comput. Sci., 2020)

Formal Verification of Bit-Vector Invertibility Conditions in Coq. - Burak Ekici; Arjun Viswanathan 001; Yoni Zohar; Cesare Tinelli; Clark W. Barrett (FroCoS, 2023)

A Sound Definitional Interpreter for a Simply Typed Functional Language. - Burak Ekici (Axioms, 2023)

Completeness of Asynchronous Session Tree Subtyping in Coq. - Burak Ekici; Nobuko Yoshida (ITP, 2024)

https://github.com/ekiciburak/sessionTreeST/tree/localtype. - Burak Ekici; Nobuko Yoshida (DROPS Artifacts, 2024)