Olivier Danvy

Research interests:

Programming and programming languages in general
and functional programming (Scheme, ML), partial evaluation, and continuations in particular.

Teaching:

• During the fourth quarter of 2007-2008, this spring,
  I have been teaching the undergraduate course on programming languages.
• During the first quarter of 2008-2008, this fall,
  I will be teaching the graduate course on Thesis Preparation (TP).
• During the third quarter of 2008-2009, next spring,
  I will be teaching a graduate course on functional-programming techniques.

Whereabouts:

• In May, I attended the Sixth International Summer School on Advanced Functional Programming.
• In July, I am attending WoLLIC 2008 in Edinburgh and
  a Summer School on Logic and Theorem Proving in Programming Languages in Oregon.

Service:

• Higher-Order and Symbolic Computation (HOSC) -- its local home page and its mirror at SRI
  (née LISP and Symbolic Computation).
• The IFL advisory committee.
• The Journal of Functional Programming.
• The Journal of Computing Science and Engineering.

Work:

`Lektor' (associate professor) in the Department of Computer Science at the University of Aarhus in Aarhus, Denmark.

Education:

• My other mother (alma mater) is the Université Pierre et Marie Curie (Paris VI) in Paris, France
  (PhD degree in Computer Science, June 1986; Habilitation, January 1993).
• My other mother-in-law (alma socrus) is the University of Aarhus in Aarhus, Denmark
  (Doctor Scientiarum, October 2006).

Former PhD students:

• Kristian Støvring, supervised jointly with Andrzej Filinski (October 24, 2007):
  On Reasoning Equationally: Lambda Calculi and Programs with Computational Effects
• Jan Midtgaard (June 20, 2007):
  Transformation, Analysis, and Interpretation of Higher-Order Procedural Programs.
• Kevin Millikin (May 1, 2007):
  A Structured Approach to the Transformation, Normalization and Execution of Computer Programs.
• Jooyong Lee, supervised jointly with Mogens Nielsen (February 25, 2007):
  Program Validation by Symbolic Execution.
• Mads Sig Ager (January 30, 2006):
  Partial Evaluation of String Matchers & Constructions of Abstract Machines.
• Malgorzata Biernacka (January 27, 2006):
  A Derivational Approach to the Operational Semantics of Functional Languages.
• Henning Korsholm Rohde, supervised jointly with Andrzej Filinski (December 19, 2005):
  Formal Aspects of Partial Evaluation.
• Dariusz Biernacki (December 15, 2005):
  The Theory and Practice of Programming Languages with Delimited Continuations.
• Bernd Grobauer (August 31, 2001):
  Topics in Semantics-based Program Manipulation.
• Lasse R. Nielsen (August 31, 2001):
  A Study of Defunctionalization and Continuation-Passing Style.
• Zhe Yang, supervised jointly with the late Robert Paige (August 21, 2001):
  Language Support for Program Generation: Reasoning, Implementation, and Applications.
• Daniel Damian (August 17, 2001):
  On Static and Dynamic Control-Flow Information in Program Analysis and Transformation.
• Morten Rhiger (August 17, 2001):
  Higher-Order Program Generation.
• Academic genealogy.

Former recent MSc students:

• Jacob Johannsen (June 25, 2008):
  An Investigation of Abadi and Cardelli's Untyped Calculus of Objects.
• Johan Munk (May 23, 2007):
  A Study of Syntactic and Semantic Artifacts and its Application to Lambda Definability, Strong Normalization, and Weak Normalization in the Presence of State.

Profile:

Daimiposten, December 2001.

Address:

Department of Computer Science, University of Aarhus
IT-parken, Aabogade 34, DK-8200 Aarhus N, Denmark
E-mail: danvy hat daimi.au.dk
Office: Room 228, Turing building
Phone (direct): (+45) 89 42 93 39
Fax (departmental): (+45) 89 42 56 01

Recent work:

• Inter-Deriving Semantic Artifacts for Object-Oriented Programming
  with Jacob Johannsen
  (June 2008 -- to appear in the proceedings of WoLLIC 2008, extended version).
• Refunctionalization at Work
  with Kevin Millikin
  (March 2007 -- to appear in SCP, extended version).
• A Simple Application of Lightweight Fusion to Proving the Equivalence of Abstract Machines
  with Kevin Millikin
  (March 2007 -- IPL 106(3):100-109, 2008, extended version).
• On One-Pass CPS Transformations
  with Kevin Millikin
  (March 2007 -- JFP 17(6):793-812, 2007, extended version).
• A Rational Deconstruction of Landin's J Operator
  with Kevin Millikin
  (December 2006 -- accepted in LMCS, preliminary version).
• A Dynamic Continuation-Passing Style for Dynamic Delimited Continuations
  with Dariusz Biernacki and Kevin Millikin
  (October 2006 -- accepted in TOPLAS, preliminary version).
• An Analytical Approach to Programs as Data Objects
  (April 2006).
• A Concrete Framework for Environment Machines
  with Malgorzata Biernacka
  (February 2006 -- TOCL 9(1):1-30, Article #6, 2007, extended version).
• A Syntactic Correspondence between Context-Sensitive Calculi and Abstract Machines
  with Malgorzata Biernacka
  (December 2005 -- TCS 375:76-108, 2007, extended version).
• On the Static and Dynamic Extents of Delimited Continuations
  with Dariusz Biernacki and Chung-chieh Shan
  (December 2005 -- SCP 60(3):274-297, 2006, extended version).
• On Obtaining the Boyer-Moore String-Matching Algorithm by Partial Evaluation
  with Henning Korsholm Rohde
  (September 2005 -- IPL 99(4):158-162, 2006, extended version).
• A Simple Proof of a Folklore Theorem about Delimited Control
  with Dariusz Biernacki
  (August 2005 -- JFP 16(3):269-280, 2006, extended version).
• An Operational Foundation for Delimited Continuations in the CPS Hierarchy
  with Malgorzata Biernacka and Dariusz Biernacki
  (August 2005 -- LMCS 1(2:5):1-39, 2005, extended version).
• Program extraction from proofs of weak head normalization
  with Malgorzata Biernacka and Kristian Støvring
  (April 2005 -- MFPS XXI, 2005, extended version).
• There and Back Again
  with Mayer Goldberg
  (January 2005 -- Fundamenta Informatica 66(4):397-413, 2005, extended version).
• Sur un exemple de Patrick Greussay
  (December 2004, at long last).
• Fast Partial Evaluation of Pattern Matching in Strings
  with Mads Sig Ager and Henning Korsholm Rohde
  (December 2004 -- TOPLAS 28(4):696-714, 2006, extended version).
• CPS Transformation of Beta-Redexes
  with Lasse R. Nielsen
  (December 2004 -- IPL 94(5):217-224, 2005, extended version).
• From Reduction-Based to Reduction-Free Normalization
  (December 2004 -- invited talk at WRS 2004).
• A Functional Correspondence between Monadic Evaluators
  and Abstract Machines for Languages with Computational Effects
  with Mads Sig Ager and Jan Midtgaard
  (December 2004 -- TCS 342(1):149-172, 2005, extended version).
• Refocusing in Reduction Semantics
  with Lasse R. Nielsen
  (November 2004).
• Lambda-Lifting in Quadratic Time
  with Ulrik P. Schultz
  (June 2004 -- JFLP 2004(1), extended version).
• From Interpreter to Logic Engine by Defunctionalization
  with Dariusz Biernacki
  (March 2004 -- LOPSTR 2003, extended version).
• A Functional Correspondence between Call-by-Need Evaluators
  and Lazy Abstract Machines
  with Mads Sig Ager and Jan Midtgaard
  (February 2004 -- IPL 90(5):223-232, 2004, extended version).
• On Evaluation Contexts, Continuations, and the Rest of the Computation
  (January 2004 -- invited talk at CW'04).
• A Rational Deconstruction of Landin's SECD Machine
  Recipient of the 2004 Peter Landin prize
  (October 2003 -- IFL'04).
• From Interpreter to Compiler and Virtual Machine: a Functional Derivation
  with Mads Sig Ager, Dariusz Biernacki, and Jan Midtgaard
  (March 2003).
• A Functional Correspondence between Evaluators and Abstract Machines
  with Mads Sig Ager, Dariusz Biernacki, and Jan Midtgaard
  (March 2003 -- PPDP'03, preliminary version).
• A New One-Pass Transformation into Monadic Normal Form
  (December 2002 -- CC'03, extended version).
• A simple CPS Transformation of Control-Flow Information
  with Daniel Damian
  (December 2001 -- Logic Journal of the IGPL 10(5):501-515, 2002, extended version).
• Syntactic Accidents in Program Analysis: On the Impact of the CPS Transformation
  with Daniel Damian
  (December 2001 -- JFP 13(5):867-904 -- extended version).
• A First-Order One-Pass CPS Transformation
  with Lasse R. Nielsen
  (December 2001 -- TCS 308(1-3):239-257, 2003, extended version).
• CPS Transformation of Flow Information, Part II: Administrative Reductions
  with Daniel Damian
  (October 2001 -- JFP 13(5):925-934, 2003, extended version).
• Defunctionalization at Work
  with Lasse R. Nielsen
  (July 2001 -- PPDP'01, extended version).
• A Unifying Approach to Goal-Directed Evaluation
  with Bernd Grobauer and Morten Rhiger
  (July 2001 -- New Generation Computing 20(1):53-73, 2002, extended version).
• Normalization by Evaluation with Typed Abstract Syntax
  with Morten Rhiger and Kristoffer Rose (May 2001 -- JFP 11(6):673-680, 2001, extended version).
• Type-directed Partial Evaluation
  (July 1999 -- lecture notes).
• Functional Unparsing
  (May 1998 -- JFP 8(6):621-625, 1998, extended version).
• Most of my papers prior to 1996.
• The BRICS publications, my own page there, and
  my list of publications from the DBLP Bibliography Server.

Slides:

• Issues about giving a talk and attending one,
  about reading a paper and writing one, and
  about receiving a review and offering one.
• Many Happy Returns.
  Slides of an invited talk at TLCA 2001 about continuations.
  (Also as a ps file and as a gzip'ed ps file.)
• The Mechanical Evaluation of Higher-Order Expressions.
  Slides of a talk at MFPS 1998 in the Peter Landin session.
  (Also as a ps file and as a gzip'ed ps file.)

Forthcoming events:

• WoLLIC 2008.
• The Summer School on Logic and Theorem Proving in Programming Languages.
• ICFP 2008.

Recent events:

• The Sixth International Summer School on Advanced Functional Programming (AFP'08),
  Nijmegen, The Netherlands, May 19-24, 2008.
• The Neilfest and my contribution there,
  Copenhagen, Denmark, August 25-26, 2007.
• The Festschrift for John Reynolds's 70th birthday.
• The 8th International Conference on Mathematics of Program Construction (MPC '06),
  Kuressaare, Estonia, July 3-5, 2006.
• The 17th Nordic Workshop on Programming Theory,
  Copenhagen, Denmark, October 19-25, 2005.
• The 10th ACM SIGPLAN International Conference on Functional Programming (ICFP 2005),
  Tallinn, Estonia, September 26-28, 2005.
• The 17th International Workshop on the Implementation and Application of Functional Languages (IFL'05),
  Dublin, Ireland, September 19-21, 2005.
• The third APPSEM II Workshop (APPSEM05),
  Frauenchiemsee, Germany, September 12-15, 2005.
• The Summer School on Program Analysis and Transformation (PAT 2005),
  Copenhagen, Denmark, June 6-10, 2005.
• The APPSEM-II Workshop on the Krivine and Zinc Abstract Machines (KAZAM),
  Birmingham, UK, May 17, 2005.
• The 10th Estonian Winter School in Computer Science (EWSCS'05).
• The 16th International Workshop on Implementation and Application of Functional Languages (IFL'04).
• The Fourth International Workshop on Reduction Strategies in Rewriting and Programming (WRS 2004).
• The Second APPSEM Workshop on Normalization by Evaluation (NBE 2004).
• The Fourth ACM SIGPLAN Workshop on Continuations (CW 2004), with pictures.
• Le colloque scientifique en l'honneur de Jean-François Perrot.

Miscellany:

• The pi-lambda seminar and its transmogrification, the PL Seminar.
• Binaries (ah, nature).
• The HOSC special issue dedicated to Christopher Strachey (Free Online Sample Copy).
• APPSEM I and APPSEM II.
• Chez Scheme and The Scheme Programming Language.
• DrScheme.
• Standard ML of New Jersey.
• The O'Caml language.
• The Coq proof assistant.
• Captain Abstraction.
• Alan Perlis's Epigrams in Programming.
• The Strachey Lectures in Computing Science at Oxford University.
• Richard P. Feynman about evaluation committees.

• C. Lee Giles and Isaac G. Councill's article
  Who gets acknowledged: Measuring scientific contributions through automatic acknowledgment indexing
  in the Proceedings of the National Academy of Sciences of the United States of America,
  101(51) pp. 17599-17604, December 21, 2004.
• Declan Butler's article about it,
  Acknowledgements hit the limelight,
  in Nature, Vol. 432, December 16, 2004.

About acknowledgment indexing:

If commenting someone else's work starts to be worth some credit,
it will encourage people to comment each other's work some more,
which will mechanically lead to better results
and, in all likelihood, to a better world.

Spinoffs:

• Declan Butler's article Frenchman is most thanked computer scientist,
  in Nature, Vol. 432, p. 790, December 16, 2004; doi:10.1038/432790b
• "Thanks God the French exist."
  Woody Allen, Hollywood Ending

A sample of acknowledgments:

• "First of all, I would like to express appropriate thanks to my editor."
  Samuel R. Delany (to the best of my memory)
• "Lastly, I acknowledge Michael A. Burstein for no particular reason."
  Timothy P. Szczesuil
• "My friends, I am highly gratified by this magnificient display of effusion."
  Captain Spaulding
• "I want to thank you for making this day necessary."
  Yogi Berra
• The acknowledgments in the scsh manual.
  Olin Shivers
• "Non merci! non merci! non merci!"
  Cyrano de Bergerac