Zobrazeno 1 - 10
of 270
pro vyhledávání: '"Subject reduction"'
Autor:
Marco Benini
Publikováno v:
Mathematics for Computation (M4C) ISBN: 9789811245213
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::31458fcaae2f960723fdff698678d96b
https://hdl.handle.net/11383/2153452
https://hdl.handle.net/11383/2153452
Autor:
Gianluca Curzi, Luca Roversi
Publikováno v:
Theoretical Computer Science. 837:26-53
We introduce $\mathsf{LEM}$, a type-assignment system for the linear $ \lambda $-calculus that extends second-order $\mathsf{IMLL}_2$, i.e., intuitionistic multiplicative Linear Logic, by means of logical rules that weaken and contract assumptions, b
Autor:
Francesco A. Genco, Federico Aschieri
Publikováno v:
POPL 2020
POPL 2020, Jan 2020, New Orleans, Louisiana, United States
POPL 2020, Jan 2020, New Orleans, Louisiana, United States
International audience; Along the lines of Abramsky's "Proofs-as-Processes" program, we present an interpretation of multiplicative linear logic as typing system for concurrent functional programming. In particular, we study a linear multiple-conclus
Autor:
Federico Aschieri
Publikováno v:
Electronic Proceedings in Theoretical Computer Science, Vol 293, Iss Proc. DCM 2018 and ITRS 2018, Pp 29-37 (2019)
Refining and extending previous work by Retor\'e, we develop a systematic approach to intersection types via natural deduction. We show how a step of beta reduction can be seen as performing, at the level of typing derivations, Prawitz reductions in
Publikováno v:
IFL
System I is a simply-typed lambda calculus with pairs, extended with an equational theory obtained from considering the type isomorphisms as equalities. In this work we propose an extension of System I to polymorphic types, adding the corresponding i
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::47a6d34a2f24061970c7bfcf50d9c726
http://arxiv.org/abs/2101.03215
http://arxiv.org/abs/2101.03215
Publikováno v:
Lecture Notes in Computer Science
23th International Conference on Coordination Languages and Models (COORDINATION)
23th International Conference on Coordination Languages and Models (COORDINATION), Jun 2021, Valletta, Malta. pp.41-60, ⟨10.1007/978-3-030-78142-2_3⟩
Lecture Notes in Computer Science ISBN: 9783030781415
COORDINATION
23th International Conference on Coordination Languages and Models (COORDINATION)
23th International Conference on Coordination Languages and Models (COORDINATION), Jun 2021, Valletta, Malta. pp.41-60, ⟨10.1007/978-3-030-78142-2_3⟩
Lecture Notes in Computer Science ISBN: 9783030781415
COORDINATION
Multiparty sessions with asynchronous communications and global types play an important role for the modelling of interaction protocols in distributed systems. In designing such calculi the aim is to enforce, by typing, good properties for all partic
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::2c34a19cca849e20da3e52dd415853fc
Autor:
Ornela Dardha, Uma Zalakain
Publikováno v:
Formal Techniques for Distributed Objects, Components, and Systems ISBN: 9783030780883
FORTE
FORTE
Linear type systems need to keep track of how programs use their resources. The standard approach is to use context splits specifying how resources are (disjointly) split across subterms. In this approach, context splits redundantly echo information
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::3c85a12d2f194d879905ec17b2f565f5
https://doi.org/10.1007/978-3-030-78089-0_9
https://doi.org/10.1007/978-3-030-78089-0_9
Publikováno v:
Formal Aspects of Component Software ISBN: 9783030906351
FACS
FACS
We introduce partial sessions and partial (multiparty) session types, in order to deal with open systems, i.e., systems with missing components. Partial sessions can be composed, and the type of the resulting system is derived from those of its compo
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::24b5b44585aa368295db1ec28f277cf6
https://doi.org/10.1007/978-3-030-90636-8_3
https://doi.org/10.1007/978-3-030-90636-8_3
Publikováno v:
Proceedings of the ACM on Programming Languages, 5(POPL)
Proceedings of the ACM on Programming Languages
Proceedings of the ACM on Programming Languages, ACM, 2021, POPL 2021, ⟨10.1145/3434341⟩
Proceedings of the ACM on Programming Languages, 2021, POPL 2021, ⟨10.1145/3434341⟩
Proceedings of the ACM on Programming Languages
Proceedings of the ACM on Programming Languages, ACM, 2021, POPL 2021, ⟨10.1145/3434341⟩
Proceedings of the ACM on Programming Languages, 2021, POPL 2021, ⟨10.1145/3434341⟩
International audience; Dependently typed programming languages and proof assistants such as Agda and Coq rely on computation to automatically simplify expressions during type checking. To overcome the lack of certain programming primitives or logica
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::a8c4c5567ed85739248561e74a81fe2b
http://resolver.tudelft.nl/uuid:14ecb3cc-e435-4e5e-afe9-a6af3d25c352
http://resolver.tudelft.nl/uuid:14ecb3cc-e435-4e5e-afe9-a6af3d25c352
Publikováno v:
Journal of Functional Programming. 31
Calculi with disjoint intersection types support a symmetric merge operator with subtyping. The merge operator generalizes record concatenation to any type, enabling expressive forms of object composition, and simple solutions to hard modularity prob