9 papers:
TLCA-2013-FridlenderP #algorithm #evaluation #normalisation #type system- A Type-Checking Algorithm for Martin-Löf Type Theory with Subtyping Based on Normalisation by Evaluation (DF, MP), pp. 140–155.
- TLCA-2011-ClairambaultD #category theory
- The Biequivalence of Locally Cartesian Closed Categories and Martin-Löf Type Theories (PC, PD), pp. 91–106.
ICALP-v1-2009-HoyrupR #effectiveness #probability- Applications of Effective Probability Theory to Martin-Löf Randomness (MH, CR), pp. 549–561.
- TLCA-2009-AwodeyR #semantics #type system
- Kripke Semantics for Martin-Löf’s Extensional Type Theory (SA, FR), pp. 249–263.
- TLCA-2005-AbelC #algorithm #framework #logic #similarity
- Untyped Algorithmic Equality for Martin-Löf’s Logical Framework with Surjective Pairs (AA, TC), pp. 23–38.
FLOPS-J1-1998-Tsukada01 #framework #type system- Martin-Löf’s Type Theory as an Open-Ended Framework (YT), pp. 31–67.
LICS-1991-Howe #on the #type system- On Computational Open-Endedness in Martin-Löf’s Type Theory (DJH), pp. 162–172.
- LICS-1988-SalvesenS #set #type system
- The Strength of the Subset Type in Martin-Löf’s Type Theory (AS, JMS), pp. 384–391.
- LICS-1987-Allen
- A Non-Type-Theoretic Definition of Martin-Löf’s Types (SA), pp. 215–221.
