Zobrazeno 1 - 1
of 1
pro vyhledávání: '"Copes, Martín"'
Publikováno v:
EPTCS 274, 2018, pp. 27-41
We present a full formalization in Martin-L\"of's Constructive Type Theory of the Standardization Theorem for the Lambda Calculus using first-order syntax with one sort of names for both free and bound variables and Stoughton's multiple substitution.
Externí odkaz:
http://arxiv.org/abs/1807.01871
