Burak Ekici

According to our database, Burak Ekici authored at least 17 papers between 2014 and 2023.

Collaborative distances:

• Dijkstra number of three.
• Erdős number of four.

2023

A Sound Definitional Interpreter for a Simply Typed Functional Language.

Burak Ekici

Axioms, January, 2023

Formal Verification of Bit-Vector Invertibility Conditions in Coq.

Burak Ekici, Arjun Viswanathan, Yoni Zohar, Cesare Tinelli, Clark W. Barrett

Proceedings of the Frontiers of Combining Systems - 14th International Symposium, 2023

2020

Mac Lane's Comparison Theorem for the Kleisli Construction Formalized in Coq.

Burak Ekici, Cezary Kaliszyk

Math. Comput. Sci., 2020

2019

Verifying Bit-vector Invertibility Conditions in Coq (Extended Abstract).

Burak Ekici, Arjun Viswanathan, Yoni Zohar, Clark W. Barrett, Cesare Tinelli

Proceedings of the Proceedings Sixth Workshop on Proof eXchange for Theorem Proving, 2019

2018

IMP with exceptions over decorated logic.

Burak Ekici

Discret. Math. Theor. Comput. Sci., 2018

Towards Mac Lane's Comparison Theorem for the (co)Kleisli Construction in Coq.

Burak Ekici

Proceedings of the Joint Proceedings of the CME-EI, 2018

Concrete Semantics with Coq and CoqHammer.

Lukasz Czajka, Burak Ekici, Cezary Kaliszyk

Proceedings of the Intelligent Computer Mathematics - 11th International Conference, 2018

2017

SMTCoq: A Plug-In for Integrating SMT Solvers into Coq.

Burak Ekici, Alain Mebsout, Cesare Tinelli, Chantal Keller, Guy Katz, Andrew Reynolds, Clark W. Barrett

Proceedings of the Computer Aided Verification - 29th International Conference, 2017

2016

Extending SMTCoq, a Certified Checker for SMT (Extended Abstract).

Burak Ekici, Guy Katz, Chantal Keller, Alain Mebsout, Andrew J. Reynolds, Cesare Tinelli

Proceedings of the Proceedings First International Workshop on Hammers for Type Theories, 2016

2015

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

Burak Ekici

PhD thesis, 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

Relative Hilbert-Post Completeness for Exceptions.

Jean-Guillaume Dumas, Dominique Duval, Burak Ekici, Damien Pous, Jean-Claude Reynaud

Proceedings of the Mathematical Aspects of Computer and Information Sciences, 2015

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

Certification of programs with computational effects.

Burak Ekici

CoRR, 2014

Program certification with computational effects.

Jean-Guillaume Dumas, Dominique Duval, Burak Ekici, Damien Pous

CoRR, 2014

Certified Proofs in Programs Involving Exceptions.

Jean-Guillaume Dumas, Dominique Duval, Burak Ekici, Jean-Claude Reynaud

Proceedings of the Joint Proceedings of the MathUI, 2014

Formal verification in Coq of program properties involving the global state effect.

Jean-Guillaume Dumas, Dominique Duval, Burak Ekici, Damien Pous

Proceedings of the 25. Journées francophones des langages applicatifs, 2014