pedrofurla.github.com

Interesting things

• https://cubical.1lab.dev/ learn about at https://twitter.com/plt_amy/status/1477725080813715458

Emily Pillmore’s PLT reading list:

• the OG Hindley-Milner-Damas paper by
  • Luis Damas and Robin Milner
  • Principal type-schemes for functional programs
  • http://web.cs.wpi.edu/~cs4536/c12/milner-damas_principal_types.pdf
• Classic Conor McBride
  • Functional Pearl: I am not a Number—I am a Free Variable
  • Conor McBride and James McKinna

  • http://www.cs.ru.nl/~james/RESEARCH/haskell2004.pdf

    In this paper, we show how to manipulate syntax with binding using a mixed representation of names for free variables (with respect to the task in hand) and de Bruijn indices for bound variables. …

• The recursion schemes approach
  • de Bruijn notation as a nested datatype
  • Richard S. Bird and Ross Paterson
  • https://www.cs.ox.ac.uk/richard.bird/online/BirdPaterson99DeBruijn.pdf
• PHOAS - Parametric Higher-Order Abstract Syntax for Mechanized Semantics
  • Adam Chlipala
  • http://adam.chlipala.net/papers/PhoasICFP08/PhoasICFP08.pdf
• Tutorial on bidi type inference - http://davidchristiansen.dk/tutorials/bidirectional.pdf
• Tutorial impl of Dep. Types - https://www.andres-loeh.de/LambdaPi/LambdaPi.pdf
• Pfenning’s notes - http://www.cs.cmu.edu/~fp/courses/15312-f04/handouts/15-bidirectional.pdf
• EdK’s bound library has a ton of comparisons - https://www.schoolofhaskell.com/user/edwardk/bound
• This paper I have not read yet, but want to - https://www.cl.cam.ac.uk/~nk480/bidir.pdf
• This one is my fave for HM tutorials - https://pdfs.semanticscholar.org/8983/233b3dff2c5b94efb31235f62bddc22dc899.pdf