Skip to Main content Skip to Navigation
Conference papers

Games and Weak-Head Reduction for Classical PCF

Abstract : We present a game model for classical PCF, a finite version of PCF extended by a catch/throw mechanism. This model is built from E-dialogues, a kind of two-players game defined by Lorenzen. In the E-dialogues for classical PCF, the strategies of the first player are isomorphic to the Böhm trees of the language. We define an interaction in E-dialogues and show that it models the weak-head reduction in classical PCF. The interaction is a variant of Coquand's debate and the weak-head reduction is a variant of the reduction in Krivine's Abstract Machine. We then extend E-dialogues to a kind of games similar to Hyland-Ong's games. Interaction in these games also models weak-head reduction. In the intuitionistic case (i.e. without the catch/throw mechanism), the extended E-dialogues are Hyland-Ong's games where the innocence condition on strategies is now a rule. Our model for classical PCF is different from Ong's model of Parigot's lambda-mu-calculus. His model works by adding new moves to the intuitionistic case while ours works by relaxing the game rules.
Document type :
Conference papers
Complete list of metadata

Cited literature [13 references]  Display  Hide  Download
Contributor : Hugo Herbelin Connect in order to contact the contributor
Submitted on : Tuesday, May 5, 2009 - 5:11:53 PM
Last modification on : Friday, February 4, 2022 - 3:08:34 AM
Long-term archiving on: : Thursday, June 10, 2010 - 10:47:06 PM


Files produced by the author(s)



Hugo Herbelin. Games and Weak-Head Reduction for Classical PCF. Typed Lambda Calculi and Applications 1997, Apr 1997, Nancy, France. pp.214--230, ⟨10.1007/3-540-62688-3⟩. ⟨inria-00381542⟩



Record views


Files downloads