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. IMP with exceptions over decorated logic.
    Burak Ekici. (submitted to DMTCS)
  2. Concrete Semantics with Coq and CoqHammer.
    Łukasz Czajka, Burak Ekici, Cezary Kaliszyk, To appear at CICM 2018.
  3. Towards Mac Lane’s Comparison Theorem for the (co)Kleisli construction in Coq.
    Burak Ekici, To appear at FMM in CICM 2018.
  4. 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,
    Proc. 29th Int. Conf. on Computer Aided Verification (CAV), pp. 126-133. Heidelberg, Germany, July 2017.
  5. Extending SMTCoq, a Certified Checker for SMT (Extended Abstract).
    Burak Ekici, Guy Katz, Chantal Keller, Alain Mebsout, Andrew Reynolds and Cesare Tinelli.,
    HaTT 2016: 1st International Workshop on Hammers for Type Theories, Coimbra, Portugal, July 2016.
  6. Hilbert-Post completeness for the state and the exception effects.
    Jean-Guillaume Dumas, Dominique Duval, Burak Ekici, Damien Pous and Jean-Claude Reynaud.,
    MACIS 2015 : Sixth International Conference on Mathematical Aspects of Computer and Information Sciences, Berlin, Germany, 11--13 November 2015.
  7. Certified proofs in programs involving exceptions. [.pdf | BibTeX]
    Jean-Guillaume Dumas, Dominique Duval, Burak Ekici and Jean-Claude Reynaud.,
    CICM 2014 : Eigth Conference on Intelligent Computer Mathematics, Coimbra, Portugal, 7--11 July 2014, CEUR Workshop Proceedings, no 1186, paper 20.
  8. Formal verification in Coq of program properties involving the global state effect. [.pdf | BibTeX]
    Jean-Guillaume Dumas, Dominique Duval, Burak Ekici and Damien Pous.,
    JFLA 2014 : Journées Francophones des Langages Applicatifs, Fréjus, France, 8--11 January 2014.

    PhD thesis

Recent Talks

  1. SMTCoq, a plug-in for the trustworthy integration of SAT/SMT solvers into Coq. Master Seminar 2 (May 2018), University of Innsbruck - Austria.
  2. Relative Hilbert-Post completeness for exceptions. Foundations Seminar, University of Ljubljana - Slovenia.
  3. IMP with exceptions over decorated logic. TFP'15, Sophia-Antipolis - France. [slides]
  4. A small talk in Casys/Meff Seminars [slides]
  5. Program certification with computational effects. JNCF'14, Marseille - France. [slides | extended abstract]
  6. Certification of programs with computational effects. CICM'14, Coimbra - Portugal. [slides | extended abstract]
  7. {IMP + Exc} over Decorated Logic. LJK, Grenoble - France.
  8. Formal verification in Coq of program properties involving the global state effect. JFLA'2014, Fréjus - France. [slides]
  9. 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]
  10. Proofs About Programs Involving Computational Effects. Exposé au LJK, Grenoble - France.
  11. Certification of Programs with Computational Effects. EJCP 2013, Dinard - France. [slides]

Misc.

    Upcoming events:

    Some past events:

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

    Curriculum Vitæ:



Last update: July 2018.