Samuel Balco

Research Software Engineer with a PhD in Computer Science, specialising in formal logics, theorem provers, functional programming languages and string diagrams.
Alt Text!


April 2022 - Present Runtime Verification

Working on the development of the symbolic execution engine used by the K Framework. Also developed the kup utility, providing simple and user friendly way to install the K framework.

Feb 2021 - 2022 Plow Technologies

Created the Inferno scripting language; an ML style programming language used by clients to process their data on the OnPing SCADA platform.

Mar 2020 - Jan 2021 University of Leicester

Worked in the bioinformatics group, led by Professor Anthony J. Brookes, on tools for data discovery and access. Built discovery tools using React on the front end and a mixture of PHP, Python and Haskell on the back end. Used Docker and CI/CD to insure build repeatabality and ease of depolyment and testing. Developed and open sourced the quickjs-hs library, used to interact with the QuickJS JavaScript engine.

Nov 2017 - Nov 2018 Wyggeston & Queen Elizabeth I College

Individual/small group drop in sessions, helping A Level students with current class topics and coursework.

Jul 2015 - Sep 2015 University of Leicester

This internship was as an extension to the work on the final year project on building an Isabelle and Scala toolbox for working with display calculi. The toolbox, developed with Prof. Alexander Kurz during my final BSc year and the graduate internship, is freely available on GitHub.

Jun 2014 - Aug 2014 University of Leicester

Received a university grant to work on formalizing simple syllogistic logics in Isabelle under the supervision of Prof. Alexander Kurz and Dr. Tom Ridge for 10 weeks during the summer break. A tutorial on the basics of Isabelle, based on the work done on the project, is available on GitHub.


Programming languages

Technologies (and other buzzwords)


Oct 2016 - Sep 2020 University of Leicester
Oct 2015 - Sep 2016 University of Oxford

Final thesis on formalizing intersection types along with proofs of subject invariance for the λ-Y calculus.

Sep 2012 - Jun 2015 University of Leicester
  • Achieved 85+% in most modules.
  • Dissertation on formalizing display calculi in Isabelle/HOL and building a supporting toolbox for reasoning about their properties in Isabelle.
  • Dissertation presented at the ALCOP 2015 conference in Delft.


Software Tool Support for Modular Reasoning in Modal Logics of Actions S. Balco, S. Frittella, G. Greco, A. Kurz, A. Palmigiano, Proc. ITP 2018
Partially monoidal categories and the algebra of simultaneous substitutions S. Balco, A. Kurz, Preprint
Nominal String Diagrams S. Balco, A. Kurz, Proc. CALCO 2019, received the best paper award
Display calculi and nominal string diagrams S. Balco, PhD thesis
Completeness of Nominal PROPs S. Balco, A. Kurz, journal version of the Nominal String Diagrams paper, under review

(Human) languages

Slovak (native speaker), English (native speaker), German (elementary proficiency).


Woodworking, electronics (e.g. Arduino, Raspberry Pi, ESP32), hacking (former member of the Nottingham hackerspace Nottinghack) and DIY (working with a laser cutter, 3D printer, interested in metalworking, etc.), swimming, skiing and playing tennis. Recently designed and helped build a fort.


Please don't hesitate to contact me using the form below:

The PDF version of this CV can be found here.

This site is protected by reCAPTCHA and the Google Privacy Policy and Terms of Service apply.