Proof and refutation in MALL as a game

Dale Miller

Description

Niveau: Supérieur
Proof and refutation in MALL as a game Dale Miller INRIA-Saclay & LIX, Ecole Polytechnique Palaiseau, France 29 September 2009 Workshop on Games, Dialogue, and Interaction University of Paris, VIII, Joint work with Olivier Delande and Alexis Saurin. Related papers appeared in MFPS 2006, LICS 2008, TCS 2009.

• purely additive


• mall without atoms


• game


• neutral expressions


• function-argument interaction

Sujets

• École polytechnique
• Saurin

Informations

• Publié par: chaeh
• Nombre de lectures: 10
• Langue: English

Extrait

ProofandrefutationinMALLasagame DaleMiller INRIA-Saclay&LIX,E ´ colePolytechnique Palaiseau,France 29September2009 WorkshoponGames,Dialogue,andInteraction UniversityofParis,VIII, http://anr-prelude.fr Related Jo p i a n p t e w rs or a k pp w e it a h red Ol i i n vie M r F D P el S an 2 d 0 e 06 a , n L d IC A S lex 2 i 0 s 0 S 8, au T ri C n S . 2009.

Outline Introduction Purelyadditivegames Theadditivefragmentof Neutralexpressions Asimpleadditivegame AgameforMALL MALLwithoutatoms Neutralexpressions Focalization Indeterminacy Thefullgame Conclusion LLAM

Gamesandproof Twostyleofgamesusedincomputerscience. Function-argumentinteraction:functionagainstenvironment. Modelsproofnormalization.Getsinterestingwithhigher-order computations.c.f.Hyland-Ong,Abramsky,fullabstractionfor .FCP Dialoguegames:Styleusedinthistalk. “IfIhaveaproof,Icanwintheargument.” AtraditionstartingwithLorenzen[1960/61],Hintikka[1968],....

!sesnefedDhPtaxalernacenooS?cigolnisemagesuyhW .detaefedsawkcattas’SR .foorpluferacadahNGecnismlacdeniamerresivdadnatnedutS . ].elpmaxeretnuocesopmocotdraobkcalbotsevoM[ . DhP m ot e sih r ,yruj o hcihw e included h kciR t Statman. r sih u defended o In1986,myfirstPhDstudent,GopalanNadathur, y smallstory e nA veilebt’nodI:SR .meroehtniamdnanoitinfiedniamymsiereH:NG