Games and Definability for FPC
McCusker, Guy
Bull. Symbolic Logic, Tome 3 (1997) no. 1, p. 347-362 / Harvested from Project Euclid
Text on Project Euclid
PDF
Alt PDF
A new games model of the language FPC, a type theory with products, sums, function spaces and recursive types, is described. A definability result is proved, showing that every finite element of the model is the interpretation of some term of the language.
Publié le : 1997-09-14
Classification:  
@article{1182353518,
     author = {McCusker, Guy},
     title = {Games and Definability for FPC},
     journal = {Bull. Symbolic Logic},
     volume = {3},
     number = {1},
     year = {1997},
     pages = { 347-362},
     language = {en},
     url = {http://dml.mathdoc.fr/item/1182353518}
}

McCusker, Guy. Games and Definability for FPC. Bull. Symbolic Logic, Tome 3 (1997) no. 1, pp.  347-362. http://gdmltest.u-ga.fr/item/1182353518/