CPL - Chalmers Publication Library
| Utbildning | Forskning | Styrkeområden | Om Chalmers | In English In English Ej inloggad.

A formalized proof of strong normalization for guarded recursive types

Andreas Abel ; Andrea Vezzosi (Institutionen för data- och informationsteknik, Datavetenskap (Chalmers))
Lecture Notes in Computer Science: 12th Asian Symposium on Programming Languages and Systems, APLAS 2014 Singapore, 17-19 November 2014 (0302-9743). Vol. 8858 (2014), p. 140-158.
[Konferensbidrag, refereegranskat]

We consider a simplified version of Nakano’s guarded fixed-point types in a representation by infinite type expressions, defined coinductively. Smallstep reduction is parametrized by a natural number “depth” that expresses under how many guards we may step during evaluation. We prove that reduction is strongly normalizing for any depth. The proof involves a typed inductive notion of strong normalization and a Kripke model of types in two dimensions: depth and typing context. Our results have been formalized in Agda and serve as a case study of reasoning about a language with coinductive type expressions.

Denna post skapades 2015-05-06. Senast ändrad 2016-10-18.
CPL Pubid: 216667


Läs direkt!

Länk till annan sajt (kan kräva inloggning)

Institutioner (Chalmers)

Institutionen för data- och informationsteknik (GU) (GU)
Institutionen för data- och informationsteknik, Datavetenskap (Chalmers)


Data- och informationsvetenskap

Chalmers infrastruktur