CV

pdf version: CV (pdf)

Lasse Letager Hansen


Curriculum Vitae
 

Contact
Information

    lasse@letager.dk

Coding Skills

Languages (1000+ hours)

  • C++

  • Python

  • Rust

Languages (100+ hours)

  • Java

  • C#

  • Haskell

  • OCaml

  • SML

  • Prolog

  • etc.

Teaching

  • Dist. Sys. and Sec.

  • Optimization

  • Formal Soft. Verif.

Conference Talks

  • CPP-2024

  • CoqPL-2024

  • TYPES-2024

  • ZKProof’7

  • NordiCrypt-2025

Language Skills

  • Danish (Native)

  • English (Fluent)

  • Chinese (A-level)

  • German (Entry)

SUMMARY


PhD in Computer Science specializing in high assurance cryptography and formal verification. Experienced software developer with strong skills in modern programming languages including C++, Rust, and Python. Passionate about building high-assurance systems with a track record of practical implementations and contributions to open-source projects. Seeking industry roles in software development, verification, research, and other technical challenging topics.

image

EXPERIENCE

PhD. Student at Aarhus University

I have been part of making frameworks to develop high assurance cryptographic protocols and primitives. These were used to implement and prove security and correctness of

  • Advanced Encryption Standard (AES),

  • Transport Layer Security (TLS), and

  • Open Vote Network (OVN) – an e-voting smart contract.

Research Assistant at Aarhus University

I formalized smart contracts by building a specification language (Hacspec) for Cryptographic protocols, which can be translated to Rocq, F* and EasyCrypt.

Junior software developer at Danske Commodities

I designed and programmed a framework for Python scrapers, and had a lot of responsibility in developing and fixing important systems.

Study Café Assistant at Egaa Gymnasium

I answered questions within science from students in the after school study cafe.

EDUCATION

CONTRIBUTION TO (OPEN-SOURCE) PROJECTS

Summer 2025

Implementing a tabled type class resolver for Rocq in Embedded λ-Prolog Interpreter (ELPI).

All of 2021-25

I have developed the Rocq backend of Hax, a Rust tool for translating code into proof assistants.

Spring 2020

My masters thesis on M-types and coinduction in cubical type theory merged into the Cubical Agda GitHub repository.

Spring 2019

I have been part of translating a simple probabilistic imperative language “pwhile” to a probabilistic ML-like language “ℛML”.

Spring 2018

I have implemented a capability machines interpreter and used capabilities to develop an inline reference monitors.

PERSONAL PROJECTS AND INTERESTS