We introduce a new approach to implicit complexity in linear logic, inspired by functional database query languages and using recent developments in effective denotational semantics of polymorphism. We give the first sub-polynomial upper bound in a type system with impredicative polymorphism; adding restrictions on quantifiers yields a characterization of logarithmic space, for which extensional completeness is established via descriptive complexity.
@InProceedings{nguyen_et_al:LIPIcs.ICALP.2019.123, author = {Nguy\~{ê}n, L\^{e} Th\`{a}nh D\~{u}ng and Pradic, C\'{e}cilia}, title = {{From Normal Functors to Logarithmic Space Queries}}, booktitle = {46th International Colloquium on Automata, Languages, and Programming (ICALP 2019)}, pages = {123:1--123:15}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-109-2}, ISSN = {1868-8969}, year = {2019}, volume = {132}, editor = {Baier, Christel and Chatzigiannakis, Ioannis and Flocchini, Paola and Leonardi, Stefano}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2019.123}, URN = {urn:nbn:de:0030-drops-106994}, doi = {10.4230/LIPIcs.ICALP.2019.123}, annote = {Keywords: coherence spaces, elementary linear logic, semantic evaluation} }
Feedback for Dagstuhl Publishing