Realizability for Peano Arithmetic with Winning Conditions in HON Games Valentin Blot ENSdeLyon April 26, 2013 ValentinBlot (ENSdeLyon) RealizabilityinHONgamesemantics April26,2013 1/23 1 Introduction 2 HON game semantics 3 Winning conditions 4 Realizability ValentinBlot (ENSdeLyon) RealizabilityinHONgamesemantics April26,2013 2/23 Introduction 1 Introduction 2 HON game semantics 3 Winning conditions 4 Realizability ValentinBlot (ENSdeLyon) RealizabilityinHONgamesemantics April26,2013 3/23 Realizability for classical logic in presence of references (cid:73) Realizers live in a model (cid:73) This model has primitive mechanisms for references (c.f. Abramsky & Honda & McCusker) (cid:73) Classical logic is obtained using a CPS translation (c.f. Laird) Definitions of winningness at the level of interactions (cid:73) Similar to modified realizability (strategies are typed) (cid:73) But winningness defined by dissecting rather than observing Adequacy and extraction for Peano arithmetic (cid:73) Interpretation of system T terms corresponding to CPS translated proofs are indeed realizers (cid:73) Extraction in the spirit of Friedman’s trick Introduction Introduction A realizability based on HON games (c.f. Hyland & Ong, Nickau) ValentinBlot (ENSdeLyon) RealizabilityinHONgamesemantics April26,2013 4/23 (cid:73) Realizers live in a model (cid:73) This model has primitive mechanisms for references (c.f. Abramsky & Honda & McCusker) (cid:73) Classical logic is obtained using a CPS translation (c.f. Laird) Definitions of winningness at the level of interactions (cid:73) Similar to modified realizability (strategies are typed) (cid:73) But winningness defined by dissecting rather than observing Adequacy and extraction for Peano arithmetic (cid:73) Interpretation of system T terms corresponding to CPS translated proofs are indeed realizers (cid:73) Extraction in the spirit of Friedman’s trick Introduction Introduction A realizability based on HON games (c.f. Hyland & Ong, Nickau) Realizability for classical logic in presence of references ValentinBlot (ENSdeLyon) RealizabilityinHONgamesemantics April26,2013 4/23 (cid:73) This model has primitive mechanisms for references (c.f. Abramsky & Honda & McCusker) (cid:73) Classical logic is obtained using a CPS translation (c.f. Laird) Definitions of winningness at the level of interactions (cid:73) Similar to modified realizability (strategies are typed) (cid:73) But winningness defined by dissecting rather than observing Adequacy and extraction for Peano arithmetic (cid:73) Interpretation of system T terms corresponding to CPS translated proofs are indeed realizers (cid:73) Extraction in the spirit of Friedman’s trick Introduction Introduction A realizability based on HON games (c.f. Hyland & Ong, Nickau) Realizability for classical logic in presence of references (cid:73) Realizers live in a model ValentinBlot (ENSdeLyon) RealizabilityinHONgamesemantics April26,2013 4/23 (cid:73) Classical logic is obtained using a CPS translation (c.f. Laird) Definitions of winningness at the level of interactions (cid:73) Similar to modified realizability (strategies are typed) (cid:73) But winningness defined by dissecting rather than observing Adequacy and extraction for Peano arithmetic (cid:73) Interpretation of system T terms corresponding to CPS translated proofs are indeed realizers (cid:73) Extraction in the spirit of Friedman’s trick Introduction Introduction A realizability based on HON games (c.f. Hyland & Ong, Nickau) Realizability for classical logic in presence of references (cid:73) Realizers live in a model (cid:73) This model has primitive mechanisms for references (c.f. Abramsky & Honda & McCusker) ValentinBlot (ENSdeLyon) RealizabilityinHONgamesemantics April26,2013 4/23 Definitions of winningness at the level of interactions (cid:73) Similar to modified realizability (strategies are typed) (cid:73) But winningness defined by dissecting rather than observing Adequacy and extraction for Peano arithmetic (cid:73) Interpretation of system T terms corresponding to CPS translated proofs are indeed realizers (cid:73) Extraction in the spirit of Friedman’s trick Introduction Introduction A realizability based on HON games (c.f. Hyland & Ong, Nickau) Realizability for classical logic in presence of references (cid:73) Realizers live in a model (cid:73) This model has primitive mechanisms for references (c.f. Abramsky & Honda & McCusker) (cid:73) Classical logic is obtained using a CPS translation (c.f. Laird) ValentinBlot (ENSdeLyon) RealizabilityinHONgamesemantics April26,2013 4/23 (cid:73) Similar to modified realizability (strategies are typed) (cid:73) But winningness defined by dissecting rather than observing Adequacy and extraction for Peano arithmetic (cid:73) Interpretation of system T terms corresponding to CPS translated proofs are indeed realizers (cid:73) Extraction in the spirit of Friedman’s trick Introduction Introduction A realizability based on HON games (c.f. Hyland & Ong, Nickau) Realizability for classical logic in presence of references (cid:73) Realizers live in a model (cid:73) This model has primitive mechanisms for references (c.f. Abramsky & Honda & McCusker) (cid:73) Classical logic is obtained using a CPS translation (c.f. Laird) Definitions of winningness at the level of interactions ValentinBlot (ENSdeLyon) RealizabilityinHONgamesemantics April26,2013 4/23 (cid:73) But winningness defined by dissecting rather than observing Adequacy and extraction for Peano arithmetic (cid:73) Interpretation of system T terms corresponding to CPS translated proofs are indeed realizers (cid:73) Extraction in the spirit of Friedman’s trick Introduction Introduction A realizability based on HON games (c.f. Hyland & Ong, Nickau) Realizability for classical logic in presence of references (cid:73) Realizers live in a model (cid:73) This model has primitive mechanisms for references (c.f. Abramsky & Honda & McCusker) (cid:73) Classical logic is obtained using a CPS translation (c.f. Laird) Definitions of winningness at the level of interactions (cid:73) Similar to modified realizability (strategies are typed) ValentinBlot (ENSdeLyon) RealizabilityinHONgamesemantics April26,2013 4/23