CV

pdf version: CV (pdf)

Lasse Letager Hansen



Curriculum Vitae
 

Contact
Information

    lasse@letager.dk

Coding Skills

Languages (100+ hours)

  • C++,

  • C#,

  • Python,

  • Rust,

  • Haskell,

  • OCaml,

  • SML,

  • Prolog

  • etc.

Teaching

  • DISSY

  • Optimization

  • FSV

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 candidate 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 helped formalize 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 helped design and program a framework for Python scrapers, and had a lot of responsibility in developing and fixing important systems.

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