Burak Ekici

I am a post-doctoral research fellow at the University of Innsbruck since February 2018. I am working with Cezary Kaliszyk and Łukasz Czajka on the coqhammer tool.

Prior to that, I was a post-doctoral research fellow at the University of Iowa in 2016. I was working with Cesare Tinelli, Chantal Keller and Alain Mebsout on the SMTCoq support for the CVC4 smt solver. See the current progress here.

Even before, I used to be a PhD student at the EDMSTII, University Joseph Fourier, in between 2013-2015, under the supervisions of Jean-Guillaume Dumas, Dominique Duval and Damien Pous.

See my previous page here.

Contact Info

e-mail: burak dot ekici at uibk dot ac dot at
University of Innsbruck,
Office 2W03, ICT building,
Technikerstr. 21a/2 6020 Innsbruck, Austria

Research Topics

Programming language semantics, computational effects, formal proofs, SMT, hammer sytems, Coq.

Code

See my github repository.

Publications

  1. Mac Lane’s Comparison Theorem for the Kleisli Construction Formalized in Coq.
    B. Ekici and C. Kaliszyk (submitted).
  2. IMP with exceptions over decorated logic.
    B. Ekici (under review at DMTCS).
  3. Concrete Semantics with Coq and CoqHammer.
    Ł. Czajka, B. Ekici and C. Kaliszyk at CICM 2018.
  4. Mac Lane’s Comparison Theorem for the Kleisli construction in Coq.
    B. Ekici at FMM in CICM 2018.
  5. 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.
  6. 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.
  7. 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.
  8. Certified proofs in programs involving exceptions. [.pdf | BibTeX]
    J.-G. Dumas, D. Duval, B. Ekici and J.-C. Reynaud at CICM 2014 (work in progress).
  9. Formal verification in Coq of program properties involving the global state effect. [.pdf | BibTeX]
    J.-G. Dumas, D. Duval, B. Ekici and D. Pous at JFLA 2014.

    PhD thesis

Recent Talks

  1. Concrete Semantics with Coq and CoqHammer. CICM 2018, Hagenberg - Austria.
  2. Mac Lane's Comparison Theorem for the (co)Kleisli construction in Coq. FMM 2018, Hagenberg - Austria.
  3. SMTCoq, a plug-in for the trustworthy integration of SAT/SMT solvers into Coq. Master Seminar 2 (May 2018), University of Innsbruck - Austria.
  4. Relative Hilbert-Post completeness for exceptions. Foundations Seminar, University of Ljubljana - Slovenia.
  5. IMP with exceptions over decorated logic. TFP'15, Sophia-Antipolis - France. [slides]
  6. A small talk in Casys/Meff Seminars [slides]
  7. Program certification with computational effects. JNCF'14, Marseille - France. [slides | extended abstract]
  8. Certification of programs with computational effects. CICM'14, Coimbra - Portugal. [slides | extended abstract]
  9. {IMP + Exc} over Decorated Logic. LJK, Grenoble - France.
  10. Formal verification in Coq of program properties involving the global state effect. JFLA 2014, Fréjus - France. [slides]
  11. Formal verification in Coq of program properties involving the global state effect.
    Séminaires LJK-Modèles et Algorithmes Déterministes: BIPOP-CASYS, Grenoble - France. [slides]
  12. Proofs About Programs Involving Computational Effects. Exposé au LJK, Grenoble - France.
  13. Certification of Programs with Computational Effects. EJCP 2013, Dinard - France. [slides]

Misc.

    Upcoming events:

    Some past events:

  1. CICM 2018: 11th Conference on Intelligent Computer Mathematics,
    RISC, Hagenberg, Austria, August 13–17, 2018.
  2. AITP 2018: 3rd Conference on Artificial Intelligence and Theorem Proving,
    Aussois, France, March 25–30, 2018.
  3. HaTT 2016: 1st International Workshop on Hammers for Type Theories, at University of Coimbra, Comibra, Portugal, 1 July 2016.
  4. My thesis defense. Find all related details here.
  5. MACIS 2015 : Sixth International Conference on Mathematical Aspects of Computer and Information Sciences at Zuse Institute, Berlin, Germany, 11--13 November 2015.
  6. Sixteenth Symposium on Trends in Functional Programming (TFP 2015) in Sophia-Antipolis, France, 03--05 June 2015.
  7. Colloque Inter'Actions 2015 en Mathématiques in Grenoble, France, 26--29 May 2015.
  8. Journées Nationales de Calcul Formel (JNCF) 2014 at CIRM, Marseille, 3--7 November 2014.
  9. Conferences on Intelligent Computer Mathematics at University of Coimbra, 7--11 July 2014.
  10. Phd school on HoTT, programming language semantics and Coq:
    Semantics of proofs and certified mathematics by Institut Henri Poincaré at CIRM, Marseille, 7--18 April 2014.
  11. JFLA: Journées Francophones des Langages Applicatifs at La-villa-clythia, Fréjus, 7--11 Januray 2014.
  12. Phd school on programming languages: École Jeunes Chercheurs en Programmation
    at Inria, Rennes, 23--31 May 2013.

    Curriculum Vitæ:



Last update: September 2018.