PeopleofSuperintelligence

Researcher

David Thrane Christiansen

Also known as David Raymond Christiansen

David Thrane Christiansen led Lean's reference manual work during a period when the Lean FRO identified AI research in mathematics and code synthesis among its goals. He completed a Ph.D. at the IT University of Copenhagen and coauthored The Little Typer. He published work on dependently typed Haskell at Galois, served as Executive Director of the Haskell Foundation, and wrote Functional Programming in Lean. As of October 2026, he is a Senior Research Software Engineer at Lean FRO.

Now at
Lean FRO
Works
7
Citations
57
h-index
3

Publication numbers from OpenAlex, as of 19 October 2026.

Timeline

  1. 2016

    A Copenhagen doctorate

    He completes a Ph.D. at the IT University of Copenhagen under Peter Sestoft in 2016.

  2. 2018

    The Little Typer

    In 2018, he and Dan Friedman publish The Little Typer, their introduction to dependent types.

  3. 2019

    Dependent Haskell at Galois

    In 2019, he and four coauthors report the challenges and benefits of using dependently typed Haskell at Galois.

  4. 2022–2023

    Leading the Haskell Foundation

    He serves as Executive Director of the Haskell Foundation from May 2022 through September 2023.

  5. 2023

    Functional Programming in Lean

    In 2023, he writes Functional Programming in Lean, a free book on programming with Lean.

  6. August 2023–July 2024

    Lean's reference manual

    He leads creation of Lean's reference manual during the FRO's first year, as the organization targets AI research in mathematics and code synthesis.

  7. As of October 2026

    Senior Research Software Engineer

    He is a Senior Research Software Engineer on the Lean FRO team.

Career

  1. NowLean FROSenior Research Software Engineer
  2. 2022–2023Haskell FoundationExecutive Director

Education

  1. 2016IT University of CopenhagenPh.D.

From the biography.

Most-cited works

  1. Elaborator reflection: extending Idris in Idris2016 · ACM SIGPLAN International Conference on Functional Programming (ICFP) · 36 citations
  2. Dependently typed Haskell in industry (experience report)2019 · Proceedings of the ACM on Programming Languages · 7 citations
  3. Extensible type-directed editing2018 · 2 citations
  4. 11 All Lists Are Created Equal2018 · 0 citations

From OpenAlex, as of 19 October 2026.

  1. More people shaping AI studied at Massachusetts Institute of Technology than at any other institutionIncludes IT University of Copenhagen. Our estimates of where the people shaping AI studied and where their careers led, from education records in cited biographies.
  2. The company share of AI researchers’ top papers rose from 2% to 32%Includes IT University of Copenhagen. We estimate where leading AI researchers worked when their most-cited papers appeared. The company share rose from 2% in 1975–1979 to 32% in 2020–2024.
  3. Google had the most people shaping AI every year from 2014 to 2025Our estimates of which organizations employed the most people shaping AI from 1961 to 2025, with a year-by-year chart.
  4. The United States employs an estimated 53% of people in our data with a known employment countryOur estimates of where AI careers are concentrated now and how countries’ shares of dated positions changed over time.

Sources and credits

Photo: We have no published photo of David Thrane Christiansen yet. Send us a free-licensed photo.

  1. David Thrane Christiansen davidchristiansen.dk. Checked 19 October 2026.
  2. Past Boards haskell.foundation. Checked 19 October 2026.
  3. 33 – David Christiansen haskell.foundation. Checked 19 October 2026.
  4. Functional Programming in Lean lean-lang.org. Checked 19 October 2026.
  5. The Lean FRO Year 1 Roadmap lean-lang.org. Checked 19 October 2026.
  6. Team — Lean Lang lean-lang.org. Checked 19 October 2026.