This book constitutes the proceedings of the 21st International Conference on Foundations of Software Science and Computational Structures, FOSSACS 2018, which took place in Thessaloniki, Greece, in April 2018, held as part of the European Joint Conference on Theory and Practice of Software, ETAPS 2018.
The 31 papers presented in this volume were carefully reviewed and selected from 103 submissions. The papers are organized in topical sections named: semantics; linearity; concurrency; lambda-calculi and types; category theory and quantum control; quantitative models; logics and equational theories; and graphs and automata.
Semantics.- Non-angelic Concurrent Game Semantics.- A Trace Semantics for System F Parametric Polymorphism.- Categorical Combinatorics for Non Deterministic Strategies on Simple Games.- A Syntactic View of Computational Adequacy.- Linearity.- A New Linear Logic for Deadlock-Free Session-Typed Processes.- A Double Category Theoretic Analysis of Graded Linear Exponential Comonads.- Depending on Session-Typed Processes.- FabULous Interoperability for ML and a Linear Language.- Concurrency.- Automata for True Concurrency Properties.- A Theory of Encodings and Expressiveness.- A Framework for Parameterized Monitorability.- Logics for Bisimulation and Divergence.- Lambda-Calculi and Types.- Call-by-need, Neededness and All That.- Fitch-Style Modal Lambda Calculi.- Realizability Interpretation and Normalization of Typed Call-by-Need.- Quotient Inductive-Inductive Types.- Category Theory and Quantum Control.- Guarded Traced Categories.- Proper Semirings and Proper Convex Functors.- From Symmetric Pattern-Matching to Quantum Control.- Quantitative Models.- The Complexity of Graph-Based Reductions for Reachability in Markov Decision Processes.- A Hierarchy of Scheduler Classes for Stochastic Automata.- Symbolically Quantifying Response Time in Stochastic Models using Moments and Semirings.- Comparator Automata in Quantitative Verification.- Logics and Equational Theories.- Modular Tableaux Calculi for Separation Theories.- Differential Calculus with Imprecise Input and its Logical Framework.- The Effects of Adding Reachability Predicates in Propositional Separation Logic.- The Equational Theory of the Natural Join and of Inner Union is Decidable.- Graphs and Automata.- Minimization of Graph Weighted Models over Circular Strings.- Games on Graphs with a Public Signal Monitoring.- WQO Dichotomy for 3-Graphs.- Verifying Higher-Order Functions with Tree Automata.
This book is Open Access under a CC BY licence.
Open Access This book is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made. The images or other third party material in this book are included in the book's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the book's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
This book constitutes the proceedings of the 21st International Conference on Foundations of Software Science and Computational Structures, FOSSACS 2018, which took place in Thessaloniki, Greece, in April 2018, held as part of the European Joint Conference on Theory and Practice of Software, ETAPS 2018.The 31 papers presented in this volume were carefully reviewed and selected from 103 submissions. The papers are organized in topical sections named: semantics; linearity; concurrency; lambda-calculi and types; category theory and quantum control; quantitative models; logics and equational theories; and graphs and automata.
Semantics.- Non-angelic Concurrent Game Semantics.- A Trace Semantics for System F Parametric Polymorphism.- Categorical Combinatorics for Non Deterministic Strategies on Simple Games.- A Syntactic View of Computational Adequacy.- Linearity.- A New Linear Logic for Deadlock-Free Session-Typed Processes.- A Double Category Theoretic Analysis of Graded Linear Exponential Comonads.- Depending on Session-Typed Processes.- FabULous Interoperability for ML and a Linear Language.- Concurrency.- Automata for True Concurrency Properties.- A Theory of Encodings and Expressiveness.- A Framework for Parameterized Monitorability.- Logics for Bisimulation and Divergence.- Lambda-Calculi and Types.- Call-by-need, Neededness and All That.- Fitch-Style Modal Lambda Calculi.- Realizability Interpretation and Normalization of Typed Call-by-Need.- Quotient Inductive-Inductive Types.- Category Theory and Quantum Control.- Guarded Traced Categories.- Proper Semirings and Proper Convex Functors.- From Symmetric Pattern-Matching to Quantum Control.- Quantitative Models.- The Complexity of Graph-Based Reductions for Reachability in Markov Decision Processes.- A Hierarchy of Scheduler Classes for Stochastic Automata.- Symbolically Quantifying Response Time in Stochastic Models using Moments and Semirings.- Comparator Automata in Quantitative Verification.- Logics and Equational Theories.- Modular Tableaux Calculi for Separation Theories.- Differential Calculus with Imprecise Input and its Logical Framework.- The Effects of Adding Reachability Predicates in Propositional Separation Logic.- The Equational Theory of the Natural Join and of Inner Union is Decidable.- Graphs and Automata.- Minimization of Graph Weighted Models over Circular Strings.- Games on Graphs with a Public Signal Monitoring.- WQO Dichotomy for 3-Graphs.- Verifying Higher-Order Functions with Tree Automata.
Inhaltsverzeichnis
Semantics.- Non-angelic Concurrent Game Semantics.- A Trace Semantics for System F Parametric Polymorphism.- Categorical Combinatorics for Non Deterministic Strategies on Simple Games.- A Syntactic View of Computational Adequacy.- Linearity.- A New Linear Logic for Deadlock-Free Session-Typed Processes.- A Double Category Theoretic Analysis of Graded Linear Exponential Comonads.- Depending on Session-Typed Processes.- FabULous Interoperability for ML and a Linear Language.- Concurrency.- Automata for True Concurrency Properties.- A Theory of Encodings and Expressiveness.- A Framework for Parameterized Monitorability.- Logics for Bisimulation and Divergence.- Lambda-Calculi and Types.- Call-by-need, Neededness and All That.- Fitch-Style Modal Lambda Calculi.- Realizability Interpretation and Normalization of Typed Call-by-Need.- Quotient Inductive-Inductive Types.- Category Theory and Quantum Control.- Guarded Traced Categories.- Proper Semirings and Proper Convex Functors.- From Symmetric Pattern-Matching to Quantum Control.- Quantitative Models.- The Complexity of Graph-Based Reductions for Reachability in Markov Decision Processes.- A Hierarchy of Scheduler Classes for Stochastic Automata.- Symbolically Quantifying Response Time in Stochastic Models using Moments and Semirings.- Comparator Automata in Quantitative Verification.- Logics and Equational Theories.- Modular Tableaux Calculi for Separation Theories.- Differential Calculus with Imprecise Input and its Logical Framework.- The Effects of Adding Reachability Predicates in Propositional Separation Logic.- The Equational Theory of the Natural Join and of Inner Union is Decidable.- Graphs and Automata.- Minimization of Graph Weighted Models over Circular Strings.- Games on Graphs with a Public Signal Monitoring.- WQO Dichotomy for 3-Graphs.- Verifying Higher-Order Functions with Tree Automata.
Klappentext
This book constitutes the proceedings of the 21st International Conference on Foundations of Software Science and Computational Structures, FOSSACS 2018, which took place in Thessaloniki, Greece, in April 2018, held as part of the European Joint Conference on Theory and Practice of Software, ETAPS 2018.
The 31 papers presented in this volume were carefully reviewed and selected from 103 submissions. The papers are organized in topical sections named: semantics; linearity; concurrency; lambda-calculi and types; category theory and quantum control; quantitative models; logics and equational theories; and graphs and automata.
