In this paper I present a partial formalisation of a normaliser for type theory in Agda Ulf Norell. Agda 2, 2007. http://www.cs.chalmers.se/\~ulfn/; extending previous work on big-step normalisation Thorsten Altenkirch and James Chapman. Big-Step Normalisation. Journal of Functional Programming, 2008. Special Issue on Mathematically Structured Functional Programming. To appear, Thorsten Altenkirch and James Chapman. Tait in one big step. In Workshop on Mathematically Structured Functional Programming, MSFP 2006, Kuressaare, Estonia, July 2, 2006, electronic Workshop in Computing (eWiC), Kuressaare, Estonia, 2006. The British Computer Society (BCS). The normaliser in written as an environment machine. Only the computational behaviour of the normaliser is presented omitting details of termination.
%0 Journal Article
%1 Chapman2009Type
%A Chapman, James
%C Amsterdam, The Netherlands, The Netherlands
%D 2009
%I Elsevier Science Publishers B. V.
%J Electron. Notes Theor. Comput. Sci.
%K 03b15-higher-order-logic-type-theory 68n15-programming-languages
%P 21--36
%R 10.1016/j.entcs.2008.12.114
%T Type Theory Should Eat Itself
%U http://dx.doi.org/10.1016/j.entcs.2008.12.114
%V 228
%X In this paper I present a partial formalisation of a normaliser for type theory in Agda Ulf Norell. Agda 2, 2007. http://www.cs.chalmers.se/\~ulfn/; extending previous work on big-step normalisation Thorsten Altenkirch and James Chapman. Big-Step Normalisation. Journal of Functional Programming, 2008. Special Issue on Mathematically Structured Functional Programming. To appear, Thorsten Altenkirch and James Chapman. Tait in one big step. In Workshop on Mathematically Structured Functional Programming, MSFP 2006, Kuressaare, Estonia, July 2, 2006, electronic Workshop in Computing (eWiC), Kuressaare, Estonia, 2006. The British Computer Society (BCS). The normaliser in written as an environment machine. Only the computational behaviour of the normaliser is presented omitting details of termination.
@article{Chapman2009Type,
abstract = {{In this paper I present a partial formalisation of a normaliser for type theory in Agda [Ulf Norell. Agda 2, 2007. http://www.cs.chalmers.se/\~{}ulfn/]; extending previous work on big-step normalisation [Thorsten Altenkirch and James Chapman. Big-Step Normalisation. Journal of Functional Programming, 2008. Special Issue on Mathematically Structured Functional Programming. To appear, Thorsten Altenkirch and James Chapman. Tait in one big step. In Workshop on Mathematically Structured Functional Programming, MSFP 2006, Kuressaare, Estonia, July 2, 2006, electronic Workshop in Computing (eWiC), Kuressaare, Estonia, 2006. The British Computer Society (BCS)]. The normaliser in written as an environment machine. Only the computational behaviour of the normaliser is presented omitting details of termination.}},
added-at = {2019-03-01T00:11:50.000+0100},
address = {Amsterdam, The Netherlands, The Netherlands},
author = {Chapman, James},
biburl = {https://www.bibsonomy.org/bibtex/2ab956025a541175921754c77ef3858aa/gdmcbain},
citeulike-article-id = {5275152},
citeulike-attachment-1 = {chapman_08_type.pdf; /pdf/user/gdmcbain/article/5275152/1118151/chapman_08_type.pdf; 7fd4c569a98c2580046090f3bf9440b090807745},
citeulike-linkout-0 = {http://portal.acm.org/citation.cfm?id=1496402},
citeulike-linkout-1 = {http://dx.doi.org/10.1016/j.entcs.2008.12.114},
day = 05,
doi = {10.1016/j.entcs.2008.12.114},
file = {chapman_08_type.pdf},
interhash = {694732ac327a13272740c69de60b8455},
intrahash = {ab956025a541175921754c77ef3858aa},
issn = {1571-0661},
journal = {Electron. Notes Theor. Comput. Sci.},
keywords = {03b15-higher-order-logic-type-theory 68n15-programming-languages},
month = jan,
pages = {21--36},
posted-at = {2017-09-18 06:17:56},
priority = {2},
publisher = {Elsevier Science Publishers B. V.},
timestamp = {2019-03-01T00:11:50.000+0100},
title = {{Type Theory Should Eat Itself}},
url = {http://dx.doi.org/10.1016/j.entcs.2008.12.114},
volume = 228,
year = 2009
}