Abstract
We present the web portal Λsymsym, available at http://158.110.146.197:31780/automata/, for experimenting with game semantics of λ^!calculus, and its normalizing elementary subcalculus, the λ^{EAL}calculus. The λ^!calculus is a generalization of the λcalculus obtained by introducing a modal operator !, giving rise to a pattern βreduction. Its subcalculus corresponds to an applicatively closed class of terms normalizing in an elementary number of steps, in which all elementary functions can be encoded. The game model which we consider is the Geometry of Interaction model I introduced by Abramsky to study reversible computations, consisting of partial involutions over a very simple language of moves.
Given a λ^! or a λ^{EAL}term, M, Λsymsym provides:
 an abstraction algorithm A^!, for compiling M into a term, A^!(M), of the linear combinatory logic CL^{!}, or the normalizing combinatory logic CL^{EAL};
 an interpretation algorithm [[ ]]^I yielding a specification of the partial involution [[A^!(M)]]^I in the model I;
 an algorithm, I2T, for synthesizing from [[A^!(M)]]^I a type, I2T([[A^!(M)]]^I), in a multimodal, intersection type assignment discipline, ⊢_!.
 an algorithm, T2I, for synthesizing a specification of a partial involution from a type in ⊢_!, which is an inverse to the former. We conjecture that ⊢_! M : I2T([[A^!(M)]]^I). Λsymsym permits to investigate experimentally the fine structure of I, and hence the game semantics of the λ^! and λ^{EAL}calculi. For instance, we can easily verify that the model I is a λ^!algebra in the case of strictly linear λterms, by checking all the necessary equations, and find counterexamples in the general case.
We make this tool available for readers interested to play with games (semantics). The paper builds on earlier work by the authors, the type system being an improvement.
BibTeX  Entry
@InProceedings{honsell_et_al:LIPIcs.TYPES.2020.7,
author = {Honsell, Furio and Lenisa, Marina and Scagnetto, Ivan},
title = {{\LambdaSymsym: An Interactive Tool for Playing with Involutions and Types}},
booktitle = {26th International Conference on Types for Proofs and Programs (TYPES 2020)},
pages = {7:17:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {9783959771825},
ISSN = {18688969},
year = {2021},
volume = {188},
editor = {de'Liguoro, Ugo and Berardi, Stefano and Altenkirch, Thorsten},
publisher = {Schloss Dagstuhl  LeibnizZentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2021/13886},
URN = {urn:nbn:de:0030drops138867},
doi = {10.4230/LIPIcs.TYPES.2020.7},
annote = {Keywords: game semantics, lambda calculus, involutions, linear logic, implicit computational complexity}
}
Keywords: 

game semantics, lambda calculus, involutions, linear logic, implicit computational complexity 
Collection: 

26th International Conference on Types for Proofs and Programs (TYPES 2020) 
Issue Date: 

2021 
Date of publication: 

07.06.2021 
Supplementary Material: 

Software (Tool): http://158.110.146.197:31780/automata/ 