Document Zbl 1452.03029

Syntax and semantics of quantitative type theory. (English) Zbl 1452.03029

Proceedings of the 2018 33rd annual ACM/IEEE symposium on logic in computer science, LICS 2018, Oxford, UK, July 9–12, 2018. New York, NY: Association for Computing Machinery (ACM). 56-65 (2018).

Cited in 17 Documents

MSC:

03B38	Type theory
03F52	Proof-theoretic aspects of linear logic and other substructural logics

Keywords:

linear logic; type theory

Cite Review PDF

Full Text: DOI Link

References:

[1]	Samson Abramsky. 1996. Retracing Some Paths in Process Algebra. In CONCUR ’96, Concurrency Theory, 7th International Conference, Pisa, Italy, August 26-29, 1996, Proceedings. 1-17. · Zbl 1514.68153
[2]	Samson Abramsky. 2005. A structural approach to reversible computation. Theor. Comput. Sci. 347, 3 (2005), 441-464. 10.1016/j.tcs.2005.07.002 · Zbl 1081.68019
[3]	Samson Abramsky, Esfandiar Haghverdi, and Philip J. Scott. 2002. Geometry of Interaction and Linear Combinatory Algebras. Mathematical Structures in Computer Science 12, 5 (2002), 625-665. 10.1017/S0960129502003730 · Zbl 1014.03056
[4]	Amal Ahmed, Matthew Fluet, and Greg Morrisett. 2007. L3: A Linear Language with Locations. Fundam. Inform. 77, 4 (2007), 397-449. http://content.iospress.com/articles/fundamenta-informaticae/fi77-4-06 · Zbl 1121.68021
[5]	Andrew Barber. 1996. Dual Intuitionistic Linear Logic. Technical Report ECS-LFCS-96-347. LFCS, University of Edinburgh.
[6]	P. N. Benton. 1994. A Mixed Linear and Non-Linear Logic: Proofs, Terms and Models (Extended Abstract). In Computer Science Logic, 8th International Workshop, CSL ’94, Kazimierz, Poland, September 25-30, 1994, Selected Papers (Lecture Notes in Computer Science), Leszek Pacholski and Jerzy Tiuryn (Eds.), Vol. 933. Springer, 121-135. · Zbl 1044.03543
[7]	Edwin Brady. 2013. Idris, a general-purpose dependently typed programming language: Design and implementation. J. Funct. Program. 23, 5 (2013), 552-593. · Zbl 1295.68059
[8]	Aloïs Brunel, Marco Gaboardi, Damiano Mazza, and Steve Zdancewic. 2014. A Core Quantitative Coeffect Calculus. In Programming Languages and Systems -23rd European Symposium on Programming, ESOP 2014. 351-370. 10.1007/978-3-642-54833-8_19 · Zbl 1405.68074
[9]	Iliano Cervesato and Frank Pfenning. 2002. A Linear Logical Framework. Inf. Comput. 179, 1 (2002), 19-75. 10.1006/inco.2001.2951 · Zbl 1031.03056
[10]	Valeria de Paiva and Eike Ritter. 2016. Fibrational Modal Type Theory. Electr. Notes Theor. Comput. Sci. 323 (2016), 143-161. 10.1016/j.entcs.2016.06.010 · Zbl 1394.03037
[11]	Peter Dybjer. 1996. Internal Type Theory. In Types for Proofs and Programs, International Workshop TYPES’95, Torino, Italy, June 5-8, 1995, Selected Papers (Lecture Notes in Computer Science), Stefano Berardi and Mario Coppo (Eds.), Vol. 1158. Springer, 120-134. · Zbl 1434.03149
[12]	Dan R. Ghica. 2007. Geometry of synthesis: a structured approach to VLSI design. In POPL. ACM, 363-375. 10.1145/1190216.1190269 · Zbl 1295.68062
[13]	Dan R. Ghica and Alex I. Smith. 2014. Bounded Linear Types in a Resource Semiring. In Programming Languages and Systems - 23rd European Symposium on Programming, ESOP 2014.331-350. 10.1007/978-3-642-54833-8_18 · Zbl 1405.68059
[14]	Jean-Yves Girard. 1987. Linear Logic. Theor. Comp. Sci. 50 (1987), 1-101. 10.1016/0304-3975(87)90045-4
[15]	Martin Hofmann. 1997. Syntax and Semantics of Dependent Types. In Semantics and Logics of Computation. Cambridge University Press, 79-130. · Zbl 0919.68083
[16]	Naohiko Hoshino. 2007. Linear Realizability. In Computer Science Logic, 21st International Workshop, CSL 2007, 16th Annual Conference of the EACSL, Lausanne, Switzerland, September 11-15, 2007, Proceedings. 420-434. · Zbl 1179.03068
[17]	Naohiko Hoshino, Koko Muroya, and Ichiro Hasuo. 2014. Memoryful geometry of interaction: from coalgebraic components to algebraic effects. In Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS ’14, Vienna, Austria, July 14-18, 2014, Thomas A. Henzinger and Dale Miller (Eds.). ACM, 52:1-52:10. 10.1145/2603088.2603124 · Zbl 1394.68062
[18]	Neelakantan R. Krishnaswami, Pierre Pradic, and Nick Benton. 2015. Integrating Linear and Dependent Types. In Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, Mumbai, India, January 15-17, 2015. 17-30. 10.1145/2676726.2676969 · Zbl 1345.68109
[19]	Ugo Dal Lago. 2011. A Short Introduction to Implicit Computational Complexity. In Lectures on Logic and Computation -ESSLLI 2010 Copenhagen, Denmark, August 2010, ESSLLI 2011, Ljubljana, Slovenia, August 2011, Selected Lecture Notes (Lecture Notes in Computer Science), Nick Bezhanishvili and Valentin Goranko (Eds.), Vol. 7388. Springer, 89-109. · Zbl 1250.03066
[20]	Ugo Dal Lago and Martin Hofmann. 2011. Realizability models and implicit complexity. Theor. Comput. Sci. 412, 20 (2011), 2029-2047. 10.1016/j.tcs.2010.12.025 · Zbl 1222.03065
[21]	Daniel R. Licata, Michael Shulman, and Mitchell Riley. 2017. A Fibrational Framework for Substructural and Modal Logics. In 2nd International Conference on Formal Structures for Computation and Deduction, FSCD 2017, September 3-9, 2017, Oxford, UK. 25:1-25:22. · Zbl 1434.03040
[22]	John Longley and Dag Normann. 2015. Higher-Order Computability. Springer. · Zbl 1471.03002
[23]	Z. Luo and Y. Zhang. 2016. A Linear Dependent Type Theory. In TYPES 2016.
[24]	The Coq development team. 2017. The Coq proof assistant reference manual. Logical Project. http://coq.inria.fr Version 8.6.
[25]	Conor McBride. 2016. I Got Plenty o’ Nuttin’. In A List of Successes That Can Change the World - Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday. 207-233. · Zbl 1343.68060
[26]	Alexandre Miquel. 2001. The Implicit Calculus of Constructions. In TLCA. 344-359. · Zbl 0981.03029
[27]	Nathan Mishra-Linger and Tim Sheard. 2008. Erasure and Polymorphism in Pure Type Systems. In Foundations of Software Science and Computational Structures, 11th International Conference, FOSSACS 2008 (Lecture Notes in Computer Science), Roberto M. Amadio (Ed.), Vol. 4962. Springer, 350-364. · Zbl 1138.68361
[28]	Torben A. Mogensen. 1997. Types for 0, 1 or Many Uses. In Implementation of Functional Languages, 9th International Workshop, IFL’97, St. Andrews, Scotland, UK, September 10-12, 1997, Selected Papers (Lecture Notes in Computer Science), Chris Clack, Kevin Hammond, and Antony J. T. Davie (Eds.), Vol. 1467. Springer, 112-122.
[29]	Tomas Petricek, Dominic A. Orchard, and Alan Mycroft. 2014. Coeffects: a calculus of context-dependent computation. In Proceedings of the 19th ACM SIGPLAN International Conference on Functional Programming, Gothenburg, Sweden, September 1-3, 2014, Johan Jeuring and Manuel M. T. Chakravarty (Eds.). ACM, 123-135. 10.1145/2628136.2628160 · Zbl 1345.68069
[30]	Frank Pfenning. 2001. Intensionality, Extensionality, and Proof Irrelevance in Modal Type Theory. In 16th Annual IEEE Symposium on Logic in Computer Science, Boston, Massachusetts, USA, June 16-19, 2001, Proceedings. IEEE Computer Society, 221-230.
[31]	Dana S. Scott. 1976. Data Types as Lattices. SIAM J. Comput. 5,3 (1976), 522-587. · Zbl 0337.02018
[32]	Michael Shulman. 2017. Brouwer’s fixed-point theorem in real-cohesive homotopy type theory. CoRR abs:1509.07584v3 (2017). https://arxiv.org/abs/1509.07584v3 · Zbl 1390.03014
[33]	Kazushige Terui. 2001. Light Affine Calculus and Polytime Strong Normalization. In 16th Annual IEEE Symposium on Logic in Computer Science, Boston, Massachusetts, USA, June 16-19, 2001, Proceedings. 209-220.
[34]	The Agda Team. 2018. (2018). http://wiki.portal.chalmers.se/agda.
[35]	Matthijs Vákár. 2015. A Categorical Semantics for Linear Logical Frameworks. In Foundations of Software Science and Computation Structures - 18th International Conference, FoSSaCS 2015 (Lecture Notes in Computer Science), Andrew M. Pitts (Ed.), Vol. 9034. Springer, 102-116. · Zbl 1461.03014

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.