Skip to content

Instantly share code, notes, and snippets.

@phase

phase/read-dt.org

Forked from queertypes/read-dt.org
Created December 18, 2022 04:17
Show Gist options
  • Save phase/933049727d9b8c7fe95729da0d80eb66 to your computer and use it in GitHub Desktop.
Save phase/933049727d9b8c7fe95729da0d80eb66 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