Refinement типы для языка Jolie
https://doi.org/10.15514/ISPRAS-2016-28(2)-2
Аннотация
Об авторах
Александр Чичигин
Университет Иннополис
Россия
Россия
Лариса Сафина
Университет Иннополис
Россия
Россия
Мохамед Эльвакиль
Университет Иннополис
Россия
Россия
Мануэль Маццара
Университет Иннополис
Россия
Россия
Фабрицио Монтези
Университет Иннополис
Россия
Россия
Виктор Ривера
Университет Иннополис
Россия
Россия
Список литературы
1. EU Project SENSORIA. Accessed April 2016. http://www.sensoria-ist.eu/.
2. Gist of SMT constraints for the example. Accessed April 2016. https://gist.github.com/gabriel-fallen/a04c33860e2157201fa8.
3. Jolie Programming Language. Accessed April 2016. http://www.jolie-lang.org/.
4. WS-BPEL OASIS Web Services Business Process Execution Language. accessed April 2016. http://docs.oasis-open.org/wsbpel/2.0/wsbpel-specification-draft.html.
5. Power Query formula reference. Technical Report, August 2015.
6. Microsoft Research. Accessed April 2016. Z3. https://github.com/Z3Prover/z3.
7. Jesper Bengtson, Karthikeyan Bhargavan, Cedric Fournet, Andrew D. Gordon, and Sergio Maffeis. Refinement types for secure implementations. ACM Trans. Program. Lang. Syst., 33(2):8:1–8:45, February 2011.
8. Gavin M. Bierman, Andrew D. Gordon, Catalin Hritcu, and David Langworthy. Semantic subtyping with an SMT solver. In Proceedings of the 15th ACM SIGPLAN International Conference on Functional Programming, ICFP ’10, pages 105–116, New York, NY, USA, 2010. ACM.
9. Marco Carbone and Fabrizio Montesi. Deadlock-freedom-by-design: multiparty asynchronous global programming. In POPL, pages 263–274, 2013.
10. Leonardo De Moura and Nikolaj Bjørner. Z3: An efficient SMT solver. In Proc. of 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS’08/ETAPS’08, pages 337–340, Berlin, Heidelberg, 2008. Springer-Verlag.
11. David Detlefs, Greg Nelson, and James B. Saxe. Simplify: A theorem prover for program checking. J. ACM, 52(3):365–473, May 2005.
12. Joshua Dunfield. A unified system of type refinements. PhD thesis, Air Force Research Laboratory, 2007.
13. Cormac Flanagan. Hybrid type checking. In Conference Record of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’06, pages 245–256, New York, NY, USA, 2006. ACM.
14. Tim Freeman and Frank Pfenning. Refinement types for ML. SIGPLAN Not., 26(6):268–277, May 1991.
15. Claudio Guidi, Ivan Lanese, Fabrizio Montesi, and Gianluigi Zavattaro. Dynamic error handling in service oriented applications. Fundam. Inform., 95(1):73–102, 2009.
16. Claudio Guidi, Roberto Lucchi, Gianluigi Zavattaro, Nadia Busi, and Roberto Gorrieri. Sock: a calculus for service oriented computing. In ICSOC, volume 4294 of LNCS, pages 327–338. Springer, 2006.
17. Kenneth Knowles, Aaron Tomb, Jessica Gronski, Stephen N Freund, and Cormac Flanagan. Sage: Unified hybrid checking for first-class types, general refinement types, and dynamic (extended report), 2006.
18. James Lewis and Martin Fowler. Microservices: a definition of this new architectural term. Accessed April 2016. http://martinfowler.com/articles/microservices.htm.
19. Roberto Lucchi and Manuel Mazzara. A pi-calculus based semantics for WS-BPEL. J. Log. Algebr. Program., 70(1):96–118, 2007.
20. Manuel Mazzara, Faisal Abouzaid, Nicola Dragoni, and Anirban Bhattacharyya. Toward design, modelling and analysis of dynamic workflow reconfigurations – A process algebra perspective. In Web Services and Formal Methods - 8th International Workshop, WS-FM, pages 64–78, 2011.
21. Robin Milner, Joachim Parrow, and David Walker. A calculus of mobile processes, I and II. Information and Computation, 100(1):1–40, 41–77, September 1992.
22. Fabrizio Montesi. JOLIE: a Service-oriented Programming Language. Master’s thesis, University of Bologna, 2010.
23. Fabrizio Montesi. Process-aware web programming with Jolie. In Proceedings of the 28th Annual ACM Symposium on Applied Computing, SAC ’13, pages 761–763, New York, NY, USA, 2013. ACM.
24. Fabrizio Montesi and Marco Carbone. Programming Services with Correlation Sets. In Proc. of Service-Oriented Computing - 9th International Conference, ICSOC, pages 125–141, 2011.
25. Fabrizio Montesi, Claudio Guidi, and Gianluigi Zavattaro. Service-oriented programming with jolie. In Web Services Foundations, pages 81–107. 2014.
26. J. M. Nielsen. A Type System for the Jolie Language. Master’s thesis, Technical University of Denmark, 2013.
27. Mila Dalla Preda, Saverio Giallorenzo, Ivan Lanese, Jacopo Mauro, and Maurizio Gabbrielli. AIOCJ: A choreographic framework for safe adaptive distributed applications. In Software Language Engineering - 7th International Conference, SLE 2014, Västerås, Sweden, September 15-16, 2014. Proceedings, pages 161–170, 2014.
28. Larisa Safina, Manuel Mazzara, Fabrizio Montesi, and Victor Rivera. Data-driven workflows for microservices (genericity in jolie). In Proc. of the 30th IEEE International Conference on Advanced Information Networking and Applications (AINA), 2016.
Рецензия
Для цитирования:
Чичигин А., Сафина Л., Эльвакиль М., Маццара М., Монтези Ф., Ривера В. Refinement типы для языка Jolie. Труды Института системного программирования РАН. 2016;28(2):33-44. https://doi.org/10.15514/ISPRAS-2016-28(2)-2
For citation:
Tchitchigin A., Safina L., Elwakil M., Mazzara M., Montesi F., Rivera V. Refinement Types in Jolie. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2016;28(2):33-44. https://doi.org/10.15514/ISPRAS-2016-28(2)-2
Послать статью по эл. почте 