Current Projects

  • The Granule Project. An ambitious research project whose goal is to rethink the foundations of statically-typed functional programming languages by making resource sensitivity an integral aspect of the language design.
  • The StATyC Project. StATyC stands for “Static Analyses of Program Flows: Types and Certificate for Complexity”. The project aims at providing new static analysis tools based on theoretical results from Implicit computational complexity. It revolves primarily around loop optimization through an original dependency model. Application to parallel optimization are currently being investigated.


  • Static Analyses of Program Flows: Types and Certificate for Complexity
    PI: Clément Aubert, Thomas Seiller. Thomas Jefferson Fund. Start date: September 10, 2020. 2 year grant, $20,000
  • CRII:SHF: A New Foundation for Attack Trees Based on Monoidal Categories.
    PI: Harley Eades. NSF CCF: 1565557. Start date: March 01, 2016. 2 year grant, $70,221


  • Clément Aubert, Ioana Cristescu. How Reversibility Can Solve Traditional Questions: The Example of Hereditary History-Preserving Bisimulation.. 31st International Conference on Concurrency Theory, CONCUR 2020, September 1-4, 2020, Vienna, Austria (Virtual Conference)., 02 September 2020. 7:1. doi: 10.4230/LIPIcs.CONCUR.2020.7
  • Clément Aubert, Marc Bagnol. Unification and Logarithmic Space. Logical Methods in Computer Science, 31 July 2018. Volume 14, Issue 3. doi: 10.23638/LMCS-14(3:6)2018
  • Harley Eades III, Jiaming Jiang, Aubrey Bryant. On Linear Logic, Functional Programming, and Attack Trees. 29 July 2018. To Appear in the Proceedings of the Fifth International Workshop on Graphical Models for Security. [PDF]
  • Jiaming Jiang, Harley Eades III, Valeria de Paiva. On the Lambek Calculus with an Exchange Modality. 07 July 2018. Extended Abstract (8 pages): 2018 Joint Workshop on Linearity & TLLA: The 5th Workshop on Linearity and the 2nd Workshop on Trends in Linear Logic and Applications. [PDF]
  • Brent Yorgey, Richard A. Eisenberg, Harley Eades III. Explaining Type Errors. 13 January 2018. Off the Beaten Track (OBT 2018). Associated with The 45th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2018). [PDF]
  • Valeria de Paiva, Harley Eades III. Dialectica Categories for the Lambek Calculus. Lecture Notes in Computer Science: Theoretical Computer Science and General Issues, 08 January 2018. Proceedings of the Symposium on Logical Foundations of Computer Science (LFCS 2018). [PDF]
  • Valeria de Paiva, Harley Eades III. Constructive Temporal Logic, Categorically. IFCoLog Journal of Logic and its Applications, 01 February 2017. Volume 4, Number 4, Special Issue Dedicated to the Memory of Grigori Mints. [PDF]
  • Harley Eades III, Aaron Stump, Ryan McCleeary. Dualized Simple Type Theory. Logical Methods in Computer Science, 15 August 2016. Volume 12, Issue 3. doi: 10.2168/LMCS-12(3:2)2016
  • Harley Eades III, Valeria de Paiva. Multiple Conclusion Linear Logic: Cut-elimination and more. Lecture Notes in Computer Science, 04 January 2016. Proceedings of the Symposium on Logical Foundations of Computer Science (LFCS 2016). doi: 10.1007/978-3-319-27683-0_7 [PDF (with proofs)]


  • Clément Aubert, Daniele Varacca. Process, Systems and Tests: Three Layers in Concurrent Computation. 16 July 2020. arXiv: 2007.08187
  • Harley Eades III, Gianluigi Bellin. A Cointuitionistic Adjoint Logic. 19 August 2017. arXiv: 1708.05896

School of Computer and Cyber Sciences Augusta University