TY - GEN
T1 - Generalised species of rigid resource terms
AU - Tsukada, Takeshi
AU - Asada, Kazuyuki
AU - Ong, C. H.Luke
N1 - Funding Information:
The authors are grateful to Marcelo Fiore for insightful comments. They would also like to thank the anonymous reviewers for their helpful and constructive comments. This work was supported by JSPS KAKENHI Grant Numbers JP15H05706 and JP16K16004, and EPSRC EP/M023974/1.
PY - 2017/8/8
Y1 - 2017/8/8
N2 - This paper introduces a variant of the resource calculus, the rigid resource calculus, in which a permutation of elements in a bag is distinct from but isomorphic to the original bag. It is designed so that the Taylor expansion within it coincides with the interpretation by generalised species of Fiore et al., which generalises both Joyal's combinatorial species and Girard's normal functors, and which can be seen as a proof-relevant extension of the relational model. As an application, we prove the commutation between computing Böhm trees and (standard) Taylor expansions for a particular nondeterministic calculus.
AB - This paper introduces a variant of the resource calculus, the rigid resource calculus, in which a permutation of elements in a bag is distinct from but isomorphic to the original bag. It is designed so that the Taylor expansion within it coincides with the interpretation by generalised species of Fiore et al., which generalises both Joyal's combinatorial species and Girard's normal functors, and which can be seen as a proof-relevant extension of the relational model. As an application, we prove the commutation between computing Böhm trees and (standard) Taylor expansions for a particular nondeterministic calculus.
UR - http://www.scopus.com/inward/record.url?scp=85028695484&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85028695484&partnerID=8YFLogxK
U2 - 10.1109/LICS.2017.8005093
DO - 10.1109/LICS.2017.8005093
M3 - Conference contribution
AN - SCOPUS:85028695484
T3 - Proceedings - Symposium on Logic in Computer Science
BT - 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017
PB - Institute of Electrical and Electronics Engineers Inc.
T2 - 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017
Y2 - 20 June 2017 through 23 June 2017
ER -