Barral, Freiric (2008): Decidability for NonStandard Conversions in Typed LambdaCalculi. Dissertation, LMU München: Faculty of Mathematics, Computer Science and Statistics 

PDF
BarralPhd.pdf 882kB 
Abstract
This thesis studies the decidability of conversions in typed lambdacalculi, along with the algorithms allowing for this decidability. Our study takes in consideration conversions going beyond the traditional beta, eta, or permutative conversions (also called commutative conversions). To decide these conversions, two classes of algorithms compete, the algorithms based on rewriting, here the goal is to decompose and orient the conversion so as to obtain a convergent system, these algorithms then boil down to rewrite the terms until they reach an irreducible forms; and the "reduction free" algorithms where the conversion is decided recursively by a detour via a metalanguage. Throughout this thesis, we strive to explain the latter thanks to the former.
Item Type:  Theses (Dissertation, LMU Munich) 

Keywords:  typed lambda calculus, conversion, reduction, decidability, normalization by evaluation 
Subjects:  500 Natural sciences and mathematics > 510 Mathematics 500 Natural sciences and mathematics 
Faculties:  Faculty of Mathematics, Computer Science and Statistics 
Language:  English 
Date of oral examination:  6. June 2008 
1. Referee:  Hofmann, Martin 
MD5 Checksum of the PDFfile:  6c6a75927c636520ecde53b4d7e81491 
Signature of the printed copy:  0001/UMC 17635 
ID Code:  9761 
Deposited On:  09. Mar 2009 09:16 
Last Modified:  24. Oct 2020 06:27 