Skip to content

Instantly share code, notes, and snippets.

@queertypes

queertypes/read-dt.org

Last active March 16, 2024 05:49
Show Gist options
  • Star 17 You must be signed in to star a gist
  • Fork 2 You must be signed in to fork a gist
  • Save queertypes/b5c6583783fda7a875c8 to your computer and use it in GitHub Desktop.
Save queertypes/b5c6583783fda7a875c8 to your computer and use it in GitHub Desktop.
Download ZIP
Implement a Dependently Typed Language and Then Some
Raw
read-dt.org

Reading

TitleAuthor(s)Year
Intuitionistic Type TheoryPer Martin-Löf1984
On the Meanings of the Logical Constants and the Justification of the Logical LawsPer Martin-Löf1996
Notes on Simplical Homotopy TheoryAndré Joval, Myles Tierney2008
Generic Programming With Dependent TypesStephanie Weirich2010
A Model of Type Theory in Simplical SetsT. Streicher2011
Practical Erasure in Dependently Typed LanguagesMatús Tejiscák, Edwin Brady2015
On the Hierarchy of Univalent Universes: Uₙ is not n-TruncatedNicolai Kraus, Christian Sattler2013
Programming in Homotopy Type TheoryDan Licata2011
Canonicity for 2-Dimensional Type TheoryDan Licata, Robert Harper2012
Positive Inductive-Recursive DefinitionsNeil Ghani, Lorenzo Malatesta, Fredrik Norvall Forsberg2013
Theory and Application of Linear Dependent TypesMatthijs Vákár2014
Inductive-inductive DefinitionsFredrik Nordvall Forsberg2013
A Finite Axiomatization of Inductive-Recursive DefinitionsPeter Dyjber, Anton Setzer1999
Totality versus Turing-Completeness?Conor McBride2015
The View From the LeftConor McBride, James McKinna2004
Capture-Avoiding Substitution as a Nominal AlgebraMurdoch J. Gabba, Aad Mathijssen2011
How to implement dependent type theory (I, II, III)Andrej Bauer2012
A Tutorial Implementation of a Dependently Typed Lambda CalculusAndres Löh Conor McBride Wouter Swiestra2001
Simply Easy! An Implementation of a Dependently Typed Lambda CalculusAndres Löh, Conor McBride, Wouter Swiestra2007
Simpler, Easier!Lennart Augustuss2007
Idris, a General Purpose Dependently Typed Programming Language: Design and ImplementationEdwin Brady2013
OPLSS: Programming in AgdaUlf Norell2014
Normalization in Lambda-CalculusAndres Abel2012
SF: Normalization of STLCBenjamin C. Pierce, …2015
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment