Uma Zalakain

CV GitHub LinkedIn

a picture of me

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.

Professional Experience

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 operations for 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.

Academic Qualifications

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)

Uma Zalakain, Ornela Dardha

Extended abstract at Workshop on Type-Driven Development (TyDe) 2021

π with leftovers: a mechanisation in Agda

Uma Zalakain, Ornela Dardha

In Proceedings of Formal Techniques for Distributed Objects, Components, and Systems (FORTE) 2021


Type-Checking Session-Typed π-calculus with Coq

Uma Zalakain

MSc Thesis, Univesity of Glasgow, 2019

Evidence-Producing Problem Solvers in Agda

Uma Zalakain

BSc Thesis, Univesity of Strathclyde, 2018

Research Activities

Invited Talks

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