Professor Danvy received his undergraduate degree (DEUG Sciences et Structures de la Matière) at the Université de Haute Normandie, in France. His alma mater (“nourishing mother”) is the Université Pierre et Marie Curie (Paris VI), where he defended a PhD (“License to conduct research”) in 1986 and a Habilitation (“License to direct research”) in 1993. He could, however, not leave well enough alone and so he defended a DSc (“Doctorate of Science”) in 2006 at Aarhus University in Denmark, making it his alma socrus (“nourishing mother-in-law”; he is also married to a Dane in real life). Prior to that, he joined Professor Neil D Jones’s research group in the Department of Computer Science at the University of Copenhagen as an Inria-funded post-doctorate to study self-applicable partial evaluation and he stayed there two more years as an assistant professor. He then toured the United States for four years (visiting Stanford University, Indiana University, Kansas State University, and Carnegie Mellon University, and spending a summer at Yale University, another at Xerox PARC, and a third at the Oregon Graduate Institute of Science and Technology) before returning to Denmark and joining the Department of Computer Science at Aarhus University, where he contributed to the BRICS Center of Excellence and the BRICS PhD School for a decade. Throughout it all, he managed to supervise over 20 PhD students, totalling over 10 distinct nationalities, and due to the prolificity of these PhD students, he is now in position to hear the pitter patter of academic great-grandchildren’s feet. He positively loves to teach, and he concurs with Leo Rosten in that humour is the affectionate communication of insight and with Albus Dumbledore in that watching students grow is a joy. He also believes that if students can smile about something technical, they have already started to reflect about it.

Professor Danvy is interested in all aspects of programming languages, from their logic and semantics to their implementation, including programming, transforming programs, program transformations, and reasoning about programs and about program transformations (for one person’s program is another program’s data). As a Scheme programmer, he is familiar with parentheses and he is not afraid to use them. Also, for several years now, he has become convinced that the Coq Proof Assistant is the greatest thing since sliced bread and that it has the potential to transcend Computer Science college education. He is also interested in scientific communication.

• Partial Evaluation
• Continuations
• Abstract Machines
• Logic in Computer Science

Olivier Danvy:
“Nested Summations”
ACM Workshop Dedicated to Jens Palsberg on the Occasion of His 60th Birthday (JENSFEST 2024)
https://doi.org/10.1145/3694848.3694858

Olivier Danvy:
“Summa Summarum: Moessner’s Theorem without Dynamic Programming”
A Second Soul: Celebrating the Many Languages of Programming – Festschrift in Honor of Peter Thiemann’s Sixtieth Birthday (PT 2024)
https://dx.doi.org/10.4204/EPTCS.413.5

Olivier Danvy:
“Folding left and right matters: direct style. accumulators, and continuations”
Journal of Functional Programming, Volume 33, e2, 2023
https://doi.org/10.1017/S0956796822000156

Olivier Danvy:
“The Tortoise and the Hare Algorithm for Finite Lists, Compositionally”
ACM Transactions on Programming Languages & Systems, 2022
https://doi.acm.org/?doi=3564619

Olivier Danvy:
“Fold–unfold lemmas for reasoning about recursive programs using the Coq proof assistant”
Journal of Functional Programming, Volume 32, e13, 2022
https://doi.org/10.1017/S0956796822000107

Olivier Danvy:
“Getting There and Back Again”,
Fundamenta Informaticae Volume 185, Issue 2, 2022
https://fi.episciences.org/paper/view/id/9356

Olivier Danvy:
“Mystery functions: making specifications, unit tests, and implementations coexist in the mind of undergraduate students”
IFL ’19: Proceedings of the 31st Symposium on Implementation and Application of Functional Languages, Article No.: 2, pages 1–9, ACM Press, 2019
https://dx.doi.org/10.1145/3412932.3412934

Olivier Danvy:
“Folding left and right over Peano Numbers”,
Journal of Functional Programming, Volume 29, e6, 2019
https://doi.org/10.1017/S0956796819000042

Dariusz Biernacki, Olivier Danvy, and Kevin Millikin:
“A dynamic continuation-passing style for dynamic delimited continuations”,
ACM Transactions on Programming Languages and Systems, 38(1): 2:1-2:25, 2015

Christian Clausen, Olivier Danvy, and Moe Masuko:
“A characterization of Moessner’s sieve”,
Theoretical Computer Science, 546:244-256, 2014

Olivier Danvy and Ian Zerny:
“Three syntactic theories for combinatory graph reduction”,
ACM Transactions on Computational Logic, 14(4):1-29, 2013

Olivier Danvy, Peter Thiemann, and Ian Zerny:
“Circularity and lambda abstraction”,
In Atze Dijkstra and Jurriaan Hage, editors,
Liber Amicorum voor Doaitse Swierstra, pages 219-231.
Departement Informatica, Universiteit Utrecht, May 2013

Olivier Danvy, Kevin Millikin, Johan Munk, and Ian Zerny:
“On inter-deriving small-step and big-step semantics: A case study for storeless call-by-need evaluation”,
Theoretical Computer Science, 435:21-42, 2012

Luca Chiarabini and Olivier Danvy:
“A proof-theoretic account of primitive recursion and primitive iteration”,
Journal of Formalized Reasoning, 4(1):85-109, 2011

Olivier Danvy and Jacob Johannsen:
“Inter-deriving semantic artifacts for object-oriented programming”,
Journal of Computer and System Sciences, 76:302-323, 2010.

Olivier Danvy and Kevin Millikin:
“Refunctionalization at work”,
Science of Computer Programming, 74(8):534-549, 2009

Olivier Danvy:
“Towards compatible and interderivable semantic specifications for the Scheme programming language, Part I: Denotational semantics, natural semantics, and abstract machines”,
In Jens Palsberg, editor, Semantics and Algebraic Specification: Essays dedicated to Peter D. Mosses on the occasion of his 60th birthday,
number 5700 in Lecture Notes in Computer Science, pages 162-185. Springer, 2009.

Malgorzata Biernacka and Olivier Danvy:
“Towards compatible and interderivable semantic specifications for the Scheme programming language, Part II: Reduction semantics and abstract machines”,
In Jens Palsberg, editor, Semantics and Algebraic Specification: Essays dedicated to Peter D. Mosses on the occasion of his 60th birthday,
number 5700 in Lecture Notes in Computer Science, pages 186-206. Springer, 2009

Olivier Danvy, Chung-chieh Shan, and Ian Zerny:
“J is for Javascript: A direct-style correspondence between Algol-like languages and Javascript using first-class continuations”,
In Walid Taha, editor, Domain-Specific Languages, IFIP TC 2 Working Conference, DSL 2009,
number 5658 in Lecture Notes in Computer Science, pages 1-19, Oxford, UK, July 2009. IFIP, Springer

Olivier Danvy and Kevin Millikin:
“A rational deconstruction of Landin’s SECD machine with the J operator”,
Logical Methods in Computer Science, 4(4:12):1-67, 2008

Olivier Danvy and Kevin Millikin:
“On the equivalence between small-step and big-step abstract machines: a simple application of lightweight fusion”,
Information Processing Letters, 106(3):100-109, 2008

Olivier Danvy:
“From reduction-based to reduction-free normalization”,
In Pieter Koopman, Rinus Plasmeijer, and Doaitse Swierstra, editors,
Advanced Functional Programming, Sixth International School, number 5382
in Lecture Notes in Computer Science, pages 66-164, Nijmegen, The Netherlands, Springer, 2008

Olivier Danvy, Kevin Millikin, and Lasse R. Nielsen:
“On one-pass CPS transformations”,
Journal of Functional Programming, 17(6):793-812, 2007

Malgorzata Biernacka and Olivier Danvy:
“A concrete framework for environment machines”,
ACM Transactions on Computational Logic, 9(1):1-30, 2007

Malgorzata Biernacka and Olivier Danvy:
“A syntactic correspondence between context-sensitive calculi and abstract machines”,
Theoretical Computer Science, 375(1-3):76-108, 2007

Olivier Danvy and Michael Spivey:
“On Barron and Strachey’s Cartesian product function, possibly the world’s first functional pearl”,
In Ralf Hinze and Norman Ramsey, editors,
Proceedings of the 2007 ACM SIGPLAN International Conference on Functional Programming (ICFP’07),
SIGPLAN Notices, Vol. 42, No.9, pages 41-46, Freiburg, Germany, September 2007. ACM Press.

• Introduction to Computer Science
• Functional Programming and Proving
• Mechanised Reasoning
• Programming Language Design and Implementation
• Introduction to Algorithms and Data Structures
• Advanced Algorithms