Weighted relational models of typed lambda-calculi. (English) Zbl 1366.03171
Proceedings of the 2013 28th annual ACM/IEEE symposium on logic in computer science, LICS 2013, Tulane University, New Orleans, LA, USA, June 25–28, 2013. Los Alamitos, CA: IEEE Computer Society (ISBN 978-0-7695-5020-6). 301-310 (2013).
MSC:
| 03B40 | Combinatory logic and lambda calculus |
| 03F52 | Proof-theoretic aspects of linear logic and other substructural logics |
| 18C20 | Eilenberg-Moore and Kleisli constructions for monads |
| 18D20 | Enriched categories (over closed or monoidal categories) |
| 68Q55 | Semantics in the theory of computing |
References:
| [1] | R. Milner and C. Strachey, A Theory of Programming Language Semantics. Chapman and Hall, London, 1976. · Zbl 0357.68004 |
| [2] | G. D. Plotkin, “LCF considered as a programming language,” Theor. Comput. Sci., vol. 5, no. 3, pp. 223-255, 1977. · Zbl 0369.68006 |
| [3] | R. Milner, “Fully abstract models of typed lambda-calculi,” Theoretical Computer Science, vol. 4, pp. 1-22, 1977. · Zbl 0386.03006 |
| [4] | A. M. Pitts, “Operationally-based theories of program equivalence,” in Semantics and Logics of Computation, P. Dybjer and A. M. Pitts, Eds. Cambridge University Press, 1997, pp. 241-298. · Zbl 0919.68086 |
| [5] | A. Ahmed, “Step-indexed syntactic logical relations for recursive and quantified types,” in Proceedings of the 15th European conference on Programming Languages and Systems, ser. ESOP’06. Berlin, Heidelberg: Springer-Verlag, 2006, pp. 69-83. [Online]. Available: http://dx.doi.org/10.1007/11693024 6 · Zbl 1178.68146 |
| [6] | E. Moggi, “Notions of computation and monads,” Information and Computation, vol. 93, pp. 55-92, 1991. · Zbl 0723.68073 |
| [7] | M. Kwiatkowska, “On quantitative software verification,” in Proc. 16th International SPIN Workshop, ser. LNCS, C. Pasareanu, Ed., vol. 5578. Springer, 2009, pp. 2-3. |
| [8] | M. Kwiatkowska, G. Norman, and D. Parker, “PRISM 4.0: Verification of probabilistic real-time systems,” in Proc. 23rd International Conference on Computer Aided Verification (CAV’11), ser. LNCS, G. Gopalakrishnan and S. Qadeer, Eds., vol. 6806. Springer, 2011, pp. 585-591. |
| [9] | K. Chatterjee, L. Doyen, and T. A. Henzinger, “Quantitative languages,” ACM Trans. Comput. Logic, vol. 11, no. 4, pp. 23:1-23:38, Jul. 2010. [Online]. Available: http://doi.acm.org/10.1145/1805950.1805953 · Zbl 1351.68155 |
| [10] | D. Sands, “Operational theories of improvement in functional languages (extended abstract),” in Functional Programming, ser. Workshops in Computing, R. Heldal, C. K. Holst, and P. Wadler, Eds. Springer, 1991, pp. 298-311. |
| [11] | D. R. Ghica, “Slot games: a quantitative model of computation,” in Proc. of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL’05), J. Palsberg and M. Abadi, Eds. ACM, 2005, pp. 85-97. · Zbl 1369.68074 |
| [12] | J.-Y. Girard, “Linear logic,” Th. Comp. Sc., vol. 50, pp. 1-102, 1987. · Zbl 0625.03037 |
| [13] | J.-Y. Girard, “Normal functors, power series and lambda-calculus,” Ann. Pure Appl. Logic, vol. 37, no. 2, pp. 129-177, 1988. · Zbl 0646.03056 |
| [14] | V. Danos and T. Ehrhard, “Probabilistic coherence spaces as a model of higher-order probabilistic computation,” Inf. Comput., vol. 209, no. 6, pp. 966-991, 2011. · Zbl 1267.68085 |
| [15] | T. Ehrhard, M. Pagani, and C. Tasson, “The Computational Meaning of Probabilistic Coherence Spaces,” in Proceedings of the 26th Annual IEEE Symposium on Logic in Computer Science (LICS 2011), ser. IEEE Computer Society Press, M. Grohe, Ed., 2011, pp. 87-96. |
| [16] | T. Ehrhard, “Finiteness spaces,” Math. Structures Comput. Sci., vol. 15, no. 4, pp. 615-646, 2005. · Zbl 1084.03048 |
| [17] | T. Ehrhard, “On Köthe sequence spaces and linear logic,” MSCS, vol. 12, pp. 579-623, 2002. · Zbl 1025.03066 |
| [18] | J. Laird, G. Manzonetto, and G. McCusker, “Constructing differential categories and deconstructing categories of games,” Information and Computation, vol. 222, no. C, pp. 247-264, 2013. · Zbl 1269.03062 |
| [19] | V. Danos and R. Harmer, “Probabilistic game semantics,” ACM Transactions on Computational Logic, vol. 3, no. 3, pp. 359-382, Jul. 2002. · Zbl 1365.68310 |
| [20] | Y. Lafont, “Logiques, catégories et machines,” Ph.D. dissertation, Université Paris 7, 1988. |
| [21] | P.-A. Melliès, “Categorical semantics of linear logic,” Panoramas et Synthèses, vol. 27, 2009. · Zbl 1206.03052 |
| [22] | P.-A. Melliès, N. Tabareau, and C. Tasson, “An explicit formula for the free exponential modality of linear logic,” in Int. Coll. Aut., Lang. and Prog. (ICALP’09), ser. LNCS, vol. 5556. Springer, 2009, pp. 247-260. · Zbl 1248.03080 |
| [23] | M. Droste and W. Kuich, “Semirings and formal power series,” in Handbook of Weighted Automata, M. Droste, W. Kuich, and H. Vogler, Eds. Springer-Verlag, 2009, ch. 1. · Zbl 1484.68082 |
| [24] | I. Guessarian, Algebraic Semantics, ser. Lecture Notes in Computer Science. Springer, 1981, vol. 99. · Zbl 0474.68010 |
| [25] | S. Mac Lane, Categories for the Working Mathematician. Berlin: Springer-Verlag, 1971. · Zbl 0232.18001 |
| [26] | H. Barendregt, The Lambda-Calculus, its Syntax and Semantics, ser. Stud. Log. F. Math., vol. 103. North-Holland, 1984. · Zbl 0551.03007 |
| [27] | R. Amadio and P.-L. Curien, Domains and Lambda Calculi, ser. Cambridge tracts in theoretical computer science. Cambridge University Press, Jul. 1998. · Zbl 0962.03001 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
