Dragiša Žunić


[Financial systems] Abstract modelling of automated trading systems, in a way that later admits the use of methods and tools to reason about that system (ideally) in an automated way. Our model captures the common core of order matching systems, with market-price and limit-price orders, and considers ways to reason about its properties.


[Meta logical frameworks] However the main challenge, aside from formalizing models of automated trading systems (ATS) in a concurrent linear framework (CLF), is to understand meta theory behind CLF and proceed towards automated meta reasoning in CLF and Celf (a tool that implements CLF). We also use LF/Twelf.

[Possible new paths]  Designing a parallel order matching system, where batches of independent orders are matched and executed in parallel, and where price-time priority (a generalization of it) is established for incoming orders as well. I am also interested in a certified design of decentralized market models, i.e., decentralized exchanges. Both to be formalized in CLF and verified for the required properties in the same system.

R e c e n t >>>
  • Presentation from Qatar Stock Exchange (QSE) → slides
  • A presentation at CMU-Q @ QNRF project seminar, October 2018. Slides →  here
  • Article: Formalization of automated trading systems in a concurrent linear frameworkLINEARITY'18 [program] (affiliated with FCSD at FLOC) - Oxford UK, July 2018. Preprint article here
  • A congruence relation for restructuring classical terms (conf. article) - ICTCS'17, Naples, Italy - proceedings, article
  • Standard classical logic as protocol for process communication (conf. abstract) - LAP'17, Dubrovnik, Croatia - book of abstracts
  • In 2016 I joined CMU-QCarnegie Mellon University in Qatar - city of Doha
  • FINTEGRATIO - a page exploring the intersection between finance and automated reasoning
  • Recent presentations about financial systems: herehere 
  • Shape interpretation of second-order moment invariants, journal, september 2016 - here
  • Logic and Applications conference, LAP 2016, Dubrovnik [search here for presentation]
  • Computational interpretation of classical logic with explicit structural rules (with P. Lescanne and S. Ghilezan) -- [search here]
  • 2 journal articles: [1] in Information Processing Letters,  december 2013 [more info here], and [2] in Applied Mathematics and Computation [here
  • Logic and Applications, Dubrovnik, sept. 2013 [pdf]
    • A talk at the Institute of Mathematics SANU, Belgrade - Seminar for general proof theory - November 2012.  [slides here]
    • An article, in International Journal of Pattern Recognition and Artifical Intelligence, published, December 2012. [more info here]
    • An article @ International Conference of Numerical Analysis and Applied Mathematics, Greece, September 2012[more info here]
    • ISMANAM 2012 Moscow, June 2012 [here]
                >>> And by the way, I also failed often.

    C U R R E N T L Y:

    Research associate, postdoctoral
    Carnegie Mellon University Qatar (here)

    PhD from Ecole Normale Supérieure, ENS Lyon, France >> here

    F O R M E R L Y:

    Associate Professor (2014-16)
    Faculty of Computer Science, Belgrade

    Research fellow (2010-11)
    Ecole Polytechnique Fédérale de Lausanne (EPFL/Lara

    Assistant Professor (2008-12)
    Faculty of Economics and Management, Novi Sad FIMEK

    PhD student (2004-08)
    Ecole Normale Supérieure de Lyon (ENS Lyon/PLUME)

    Master in Quantitative Finance (2014-15) - no degree.
    Faculty of Economics, Belgrade (IMQF)

    Research associate
    Faculty of Technical Sciences, FTN Novi Sad (FTN/CMS)

      Драгиша Жунић
      Компјутерске науке
      Универзитет Карнеги Мелон у Катару
      Доха, Катар


    - Market design, matching markets

    - Finance in practice and in theory

    - Decentralized markets design and blockchain related concepts

    - Digital entrepreneurship and technology transfer