Synchronous Games, Simulations and lambda-calculus

Details Synchronous Games, Simulations and lambda-calculus Synchronous Games, Simulations and lambda-calculus

2009-05-25

arxiv.org/abs/0905.4066v1

Games for Logic and Programming Languages, European Conferences on Theory and Practice of Software (ETAPS 2005), Edinburgh : R

Computer Science

Logic in Computer Science

Scientific paper

We refine a model for linear logic based on two well-known ingredients: games and simulations. We have already shown that usual simulation relations form a sound notion of morphism between games; and that we can interpret all linear logic in this way. One particularly interesting point is that we interpret multiplicative connectives by synchronous operations on games. We refine this work by giving computational contents to our simulation relations. To achieve that, we need to restrict to intuitionistic linear logic. This allows to work in a constructive setting, thus keeping a computational content to the proofs. We then extend it by showing how to interpret some of the additional structure of the exponentials. To be more precise, we first give a denotational model for the typed lambda-calculus; and then give a denotational model for the differential lambda-calculus of Ehrhard and Regnier. Both this models are proved correct constructively.

Affiliated with

Also associated with

No associations

Rating

Synchronous Games, Simulations and lambda-calculus does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.

If you have personal experience with Synchronous Games, Simulations and lambda-calculus, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Synchronous Games, Simulations and lambda-calculus will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-294866