I bring a unique blend of academic insights and practical experience to any Scala or functional programming role. During my time in academia, I’ve specialised in software verification and advanced functional programming. During my time in industry, I’ve leveraged foundational functional programming principles to drive product development and simplify complex systems.
- Scala Engineer
ITV PLC, April 2022 - present
Product ITV News serves an average of over 1 million daily page views. Purely functional backend Scala stack using cats, cats-effect and fs2. Daily use of Kafka, PostgreSQL and Redis. Delivery through GA and Jenkins. Deployment through AWS, Docker, Kubernetes and Terraform. RESTful and GraphQL APIs. Significant emphasis on testing, including integration tests and property-based tests. Product development following agile processes.
Role Actively led discussions around architectural solutions. Brought forward initiatives that generalise existing ad-hoc solutions into more powerful principled ones. Created tasks aiming to strengthen backend product development. Re-engineered systems and codebases to simplify structure. Directly coordinated with stakeholders and responded to external bug reports. Assisted colleagues with functional programming queries, fostering a collaborative learning environment.
- Types and Type Changing Operations for Distributed Data Structures
Microsoft Research Cambridge, 2021
Product Research on supporting
type changing operationsfor distributed data structures. Akin to a real-time collaborative text editor, but where the data is structured and typed instead of plain text. The operations executed on the data need to be well typed and enable type changes.
Role Placement in the Calc Intelligence group, took part in their day-to-day activities. Modelled a distributed system with type changing operations, defined some of its desirable properties and mechanised proofs that show they hold.
- RISE: a functional pattern-based data-parallel language
Edinburgh University, 2021
Product RISE a functional pattern-based data-parallel language. A high-level functional Scala DSL gets compiled to high performance C, OpenMP, OpenCL and CUDA. The program is rewritten following user-defined optimisation strategies.
Role Led refactoring efforts to consolidate the existing codebase and addressed longstanding issues. Interfaced with researchers actively developing new features.
- PhD Computing Science, unfinished
University of Glasgow, 2019 - April 2022
Machine verification of typed process calculi.
Modelled typed process calculi with support for linear types, defined type safety properties, and proved they hold. Used theorem provers, dependent types and advanced functional programming techniques to mechanise the models and proofs, and verify them correct.
- MSc Computing Science, with Distinction
University of Glasgow, 2018 - 2019
- BSc Hons Computer Science, First class honours
University of Strathclyde, 2014 - 2018
Awarded Andrew McGettrick prize for outstanding performance throughout the degree (2 recipients).
Conference and Workshop Papers
- Co-Contextual Typing Inference for the Linear π-Calculus in Agda (Extended Abstract)
- π with leftovers: a mechanisation in Agda
- Type-Checking Session-Typed π-calculus with Coq
- Evidence-Producing Problem Solvers in Agda
- PLACE’22 Program committee member
- TyDe’21 sub-reviewer
- PLDI’21 artifact evaluation Program committee member
- ICE’21 Program committee member
- Proving in Constructive Mathematics by Programming in Agda (10h seminar series) (link)
Basque Center for Applied Mathematics, 2021
- Theorem Proving with Dependent Types in Agda
Formal Analysis, Theory & Algorithms Seminar, 2021
- An Introduction to Session Types
Mathematically Structured Programming 101, 2020
- Mechanising the Linear π-calculus
Languages, Systems, and Data Seminar, 2020
- π with leftovers: a mechanisation in Agda
Programming Languages at the University of Glasgow, 2020
Verification of Session Types, 2020
Agda Implementors’ Meeting, 2020
- Machine Verification with Agda
Seminar series at UoG
- Type-Checking a Session-Typed π-Calculus with Coq
Student talks at SPLV’19
Student talks at BehAPI
Tutoring and Co-Supervision
- co-supervision of MSc theses:
- Empirical study of mechanised session types, Di Cheng, 2021
- Typed Operations on Distributed Data Structures, Peng Zhao, 2021
- Encoding session types into the linear pi-calculus in Agda, Yuan Gao, 2021
- co-supervision of BSc theses:
- Encoding session types into the linear pi-calculus in Agda, Patryk Kaczmarczyk, 2020
- Abalone in Haskell, Jing Lee, 2020
- CS1P, first year programming, 2021
- CS1CT, introduction to computational thinking, 2020