Lasse Letager Hansen
Curriculum Vitae
CONTACT INFORMATION
| First name | Lasse Letager |
| Surname | Hansen |
EDUCATION
MSc in Computer Science, Aarhus University
Elected directions: Cryptography and Programming Languages
Average: 10.60 (unweighted), 10.83 (weighted) out of 12 (danish 7 point grade scale)
BSc in Computer Science, Aarhus University
Elected courses: Linear Algebra, Algebra, Machine Learning
Average: 10.38 (unweighted), 10.48 (weighted) out of 12 (danish 7 point grade scale)
STX, Egaa Gymnasium (Physics A-level, Mathematics A-level, Chemistry B-level)
COURSES
Cryptography: Cryptology, Cryptologic Protocol Theory, Cryptographic Computation
Programming Languages: Functional Programming, Language-Based Security, Program analysis and Verification
Research Projects
Spring 2020
I wrote my masters thesis on M-types and coinduction in cubical type theory/homotopy type theory formalized in Cubical Agda. As part of that I contributed to the Cubical Agda GitHub repository.
Fall 2019
I followed a reading course on homotopy type theory (HoTT), not for credit, supervised by Bas Spitters (associate professor). I also did a research project, supervised by Lars Birkedal (professor), about describing/representing co-inductive data structures in HeapLang/Iris, which taught me about modal and Hoare logic and guarded recursion.
Spring 2019
I did a research project on developing a framework for formalizing cryptography, supervised by Bas Spitters (associate professor). We constructed a translation from “pwhile” a simple probabilistic imperative language to “ℛML” a probabilistic ML-like language, which gave me insight in measure theory and the formalization of cryptography, while giving me experience in using Coq for larger projects.
Fall 2018
I did an elective course on category theory held by Lars Birkedal (professor) and Aleš Bizjak (postdoc), where we followed Steve Awodey’s book “Category Theory.” I also participated in the EUTYPES2018 conference.
Spring 2018
I did a research project, supervised by Aslan Aaskarov (associate professor) and Lau Skorstengaard (PhD.). The project was about capability machines, in the project I used the capability machines to develop a more secure implementation of inline reference monitors.
General
I have participated in most of the weekly group meetings in the research group for Logic and Semantics at Aarhus University, from 2018-2020, giving me insight into the research community.
SKILLS
Coding skills
I have devoted a lot of time coding in proof assistants: Cubical Agda for my masters, Coq for a research project in the Spring of 2019, and Iris/HeapLang for a research project in the fall of 2019. I am confident with coding, since I have spent hundreds of hours coding in multiple programming languages (C++,C#, Python, Rust, Haskell, OCaml, SML, etc.) for spare time, school and as a job.
Language skills
Danish (Native), English (Fluent), Chinese (High-school A-level), German (Entry)
PREVIOUS JOBS
Research Assistant with Bas Spitters
I am formalizing smart contracts, for that purpose we are part of creating a specification language (Hacspec) for Cryptographic protocols, which can be translated to Coq, 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.
Studycafé assistant at Egaa Gymnasium
Helping people with homework and hand-ins in a high-school study café, primarily focused on mathematics, physics, chemistry and biology.