Burak Ekici
e-mail: burak.ekici@cs.ox.ac.uk
office: Department of Computer Science, University of Oxford, Wolfson Building, Room 404.
previous employment
Publications
- Formal Verification of Bit-vector
Invertibility Conditions in Coq
B. Ekici, A. Viswanathan, Y. Zohar, C. Tinelli and C. Barrett at FroCoS 2023.
- A Sound Definitional Interpreter for a Simply Typed Functional Language
B. Ekici at Axioms, vol. 12, no. 43, January 2023.
- Formal categorical reasoning
B. Ekici at Turkish Journal of Mathematics, vol. 46, no. 4, May 2022.
- Mac Lane’s Comparison Theorem for the Kleisli Construction Formalized in Coq
B. Ekici and C. Kaliszyk at Mathematics in Computer Science, February 2020.
- Verifying Bit-vector Invertibility Conditions in Coq
B. Ekici, A. Viswanathan, Y. Zohar, C. Barrett and C. Tinelli at PxTP 2019.
- IMP with exceptions over decorated logic
B. Ekici at Discrete Mathematics and Theoretical Computer Science, vol. 20, no. 2, October 2018.
- Concrete Semantics with Coq and CoqHammer
Ł. Czajka, B. Ekici and C. Kaliszyk at CICM 2018.
-
Towards Mac Lane’s Comparison Theorem for the Kleisli construction in Coq
B. Ekici at FMM in CICM 2018.
-
SMTCoq: A plug-in for integrating SMT solvers into Coq
B. Ekici, A. Mebsout, C. Tinelli, C. Keller, G. Katz, A. Reynolds and C. Barrett at CAV 2017.
-
Extending SMTCoq, a Certified Checker for SMT (Extended Abstract)
B. Ekici, G. Katz, C. Keller, A. Mebsout, A. Reynolds and C. Tinelli at HaTT 2016.
-
Hilbert-Post completeness for the state and the exception effects
J.-G. Dumas, D. Duval, B. Ekici, D. Pous and J.-C. Reynaud at MACIS 2015.
-
Certified proofs in programs involving exceptions
J.-G. Dumas, D. Duval, B. Ekici and J.-C. Reynaud at CICM 2014 (work in progress).
-
Formal verification in Coq of program properties involving the global state effect
J.-G. Dumas, D. Duval, B. Ekici and D. Pous at JFLA 2014.
PhD thesis
Teaching
- Main Course: Operating Systems (2022-2023)
- Main Course: Programming Language Concepts (2019-2020, 2022-2023)
- Main Course: Formal Languages and Abstract Machines (2020··2023)
- Main Course: Functional Programming (2022-2023)
- Main Course: Category Theory in Computer Science (2021-2022)
- Main Course: Fundamentals of Programming I (2021-2022)
- Main Course: Digital Design (2019-2020)
- Main Course: Microprocessors (2019-2020)
- Proseminar:
Discrete Mathematics (2018-2019)
Recent Talks
Software development
Curriculum Vitae