Burak Ekici

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

I completed my PhD in December 2015 at the EDMSTII, University Joseph Fourier under the supervisions of Jean-Guillaume Dumas, Dominique Duval and Damien Pous.

See my previous page here.

Contact Info

e-mail: burak dash ekici at uiowa dot edu
office: Department of Computer Science
The University of Iowa
14 MacLean Hall
Iowa City, IA 52242, USA

bureau: MLH 201N

Research Topics

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

Code

See my github repository.

Publications

  1. SMTCoq: A plug-in for integrating SMT solvers into Coq (submitted).

  2. 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.
  3. 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.
  4. IMP with exceptions over decorated logic.
    Burak Ekici. (presented at TFP 2015)
  5. 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.
  6. 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.
  7. Implementation of Search Strategies in Control Network Programming. [.pdf]
    K. Kratchanov, E. Golemanova, T. Golemanov, T. Ercan, B. Ekici.,
    Procedural and Non-Procedural In: Proc. Intl. Symposium in Innovations in Intelligent Systems
    and Applications (INISTA 2010), June 2010, Kayseri, Turkey, 386-390.
  8. Implementations of Category Theory in Computer Science.
    Ekici B., Yucel C., Kilinc G., Koltuksuz A.,
    9th National Mathematics Symposium, Karadeniz Technical University, October 2010 (In Turkish).

    PhD thesis

Recent Talks

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

Misc.

    Upcoming events:

    Some past events:

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

    Curriculum Vitæ:



Last update: February 2017.