| CARVIEW |
Presentation
I am a Chancellor's Fellow in the Mathematically Structured Programming Group at the University of Strathclyde in Glasgow (Scotland).
Prior to that I was a Research Fellow working together with Edwin Brady on the dependently typed programming language Idris 2 at the University of St Andrews (Scotland).
Research interests
I am passionate about building trustworthy systems, and developing the languages, programming patterns, libraries, and tools that make it easier to develop such systems in an interactive manner.
I have a particular focus on efficient runtime representations, generic programming, proof automation, and user experience. You can read more about it in my research programme.
Software
On top of being an Idris 2 maintainer, I have been a core contributor to Agda, its standard library and have published various libraries taking advantage of dependent types to define e.g. total parsers, or declarative hierarchical command line interfaces.
News
- The Agda standard library: version 2.0 in the Journal of Open Source Software
- Member of ITP 2026's Program Committee
- Frex: dependently-typed algebraic simplification at ICFP 2025 in Singapore
- Speaker at TYPES 2025
- Member of ICFP 2025's Program Committee
- Member of GPCE 2025's Program Committee
- Member of TYPES 2025's Program Committee
- Speaker at BOB Konf 2025
- Invited speaker at TUPLES 2025
- Invited guest of the December 2024 IFIP WG 2.11 meeeting in Edinburgh
- Co-chair of PEPM 2025
- Member of TyDe 2024's Program Committee
- Co-organising the 2024 edition of the Scottish Programming Languages and Verification summer school in Glasgow
- Scoped and Typed Staging by Evaluation at PEPM 2024 in London
Last update: 2026 01
