Foundations of Software Science and Computation Structures : : 23rd International Conference, FOSSACS 2020, Held As Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, April 25-30, 2020, Proceedings.
Saved in:
Superior document: | Lecture Notes in Computer Science Series ; v.12077 |
---|---|
: | |
TeilnehmendeR: | |
Place / Publishing House: | Cham : : Springer International Publishing AG,, 2020. ©2020. |
Year of Publication: | 2020 |
Edition: | 1st ed. |
Language: | English |
Series: | Lecture Notes in Computer Science Series
|
Online Access: | |
Physical Description: | 1 online resource (657 pages) |
Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
id |
5006702647 |
---|---|
ctrlnum |
(MiAaPQ)5006702647 (Au-PeEL)EBL6702647 (OCoLC)1239981377 |
collection |
bib_alma |
record_format |
marc |
spelling |
Goubault-Larrecq, Jean. Foundations of Software Science and Computation Structures : 23rd International Conference, FOSSACS 2020, Held As Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, April 25-30, 2020, Proceedings. 1st ed. Cham : Springer International Publishing AG, 2020. ©2020. 1 online resource (657 pages) text txt rdacontent computer c rdamedia online resource cr rdacarrier Lecture Notes in Computer Science Series ; v.12077 Intro -- ETAPS Foreword -- Preface -- Organization -- Contents -- Neural Flocking: MPC-based Supervised Learning of Flocking Controllers -- 1 Introduction -- 2 Background -- 2.1 Model-Predictive Control -- 2.2 Declarative Flocking -- 3 Additional Control Objectives -- 4 Neural Flocking -- 4.1 Training Distributed Flocking Controllers -- 5 Experimental Evaluation -- 5.1 Preliminaries -- 5.2 Results for Basic Flocking -- 5.3 Results for Obstacle and Predator Avoidance -- 5.4 DNC Generalization Results -- 5.5 Statistical Model Checking Results -- 6 Related Work -- 7 Conclusions -- References -- On Well-Founded and Recursive Coalgebras -- 1 Introduction -- 2 Preliminaries -- 2.1 Algebras and Coalgebras. -- 2.2 Preservation Properties. -- 2.3 Factorizations. -- 2.4 Chains. -- 3 Recursive Coalgebras -- 4 The Next Time Operator and Well-Founded Coalgebras -- 5 The General Recursion Theorem and its Converse -- 6 Closure Properties of Well-founded Coalgebras -- 7 Conclusions -- References -- Timed Negotiations* -- 1 Introduction -- 2 Negotiations: Definitions and Brexit example -- 3 Timed Negotiations -- 4 High level view of the main results -- 5 Deterministic Negotiations -- 6 Sound Negotiations -- 7 k-Layered Negotiations -- 7.1 Algorithmic properties -- 7.2 Minimal Execution Time -- 8 Conclusion -- References -- Cartesian Difference Categories -- 1 Introduction -- 2 Cartesian Differential Categories -- 2.1 Cartesian Left Additive Categories -- 2.2 Cartesian Differential Categories -- 3 Change Action Models -- 3.1 Change Actions -- 3.2 Change Action Models -- 4 Cartesian Difference Categories -- 4.1 Infinitesimal Extensions in Left Additive Categories -- 4.2 Cartesian Difference Categories -- 4.3 Another look at Cartesian Differential Categories -- 4.4 Cartesian Difference Categories as Change Action Models -- 4.5 Linear Maps and ε-Linear Maps. 5 Examples of Cartesian Difference Categories -- 5.1 Smooth Functions -- 5.2 Calculus of Finite Diffferences -- 5.3 Module Morphisms -- 5.4 Stream calculus -- 6 Tangent Bundles in Cartesian Di erence Categories -- 6.1 The Tangent Bundle Monad -- 6.2 The Kleisli Category of T -- 7 Conclusions and Future Work -- References -- Contextual Equivalence for Signal Flow Graphs -- 1 Introduction -- 2 Background: the Affine Signal Flow Calculus -- 2.1 Syntax -- 2.2 String Diagrams -- 2.3 Denotational Semantics and Axiomatisation -- 2.4 Affine vs Linear Circuits -- 3 Operational Semantics for Affine Circuits -- 3.1 Trajectories -- 4 Contextual Equivalence and Full Abstraction -- 4.1 From Polynomial Fractions to Trajectories -- 4.2 Proof of Full Abstraction -- 5 Functional Behaviour and Signal Flow Graphs -- 6 Realisability -- 7 Conclusion and Future Work -- References -- Parameterized Synthesis for Fragments of First-Order Logic over Data Words -- 1 Introduction -- 2 Preliminaries -- 3 Parameterized Synthesis Problem -- 4 FO[˘] and Parameterized Vector Games -- 4.1 Satisfiability and Normal Form for FO[˘] -- 4.2 From Synthesis to Parameterized Vector Games -- 5 Results for FO[˘] via Parameterized Vector Games -- 6 Conclusion -- References -- Controlling a random population -- 1 Introduction -- 2 The stochastic control problem -- 3 The sequential ow problem -- 4 Reduction of the stochastic control problem to the sequential flow problem -- 5 Computability of the sequential ow problem -- 6 Conclusions -- Acknowledgements -- References -- Decomposing Probabilistic Lambda-Calculi -- 1 Introduction -- 1.1 Related Work -- 2 The Probabilistic Event λ-Calculus ^PE -- 3 Properties of Permutative Reduction -- 4 Confluence -- 4.1 Parallel Reduction and Permutative Reduction -- 4.2 Complete Reduction -- 5 Strong Normalization for Simply-Typed Terms. 6 Projective Reduction -- 7 Call-by-value Interpretation -- 8 Conclusions and Future Work -- Acknowledgments -- References -- On the k-synchronizability of Systems -- 1 Introduction -- 2 Preliminaries -- 3 k-synchronizable Systems -- 4 Decidability of Reachability for k-synchronizable Systems -- 5 Decidability of k-synchronizability for Mailbox Systems -- 6 k-synchronizability for Peer-to-Peer Systems -- 7 Concluding Remarks and Related works -- References -- General Supervised Learning as Change Propagation with Delta Lenses -- 1 Introduction -- 2 Background: Update propagation and delta lenses -- 2.1 Why deltas. -- 2.2 Consistency restoration via update propagation: An Example -- 2.3 Update propagation and update policies -- 2.4 Delta lenses -- 3 Asymmetric Learning Lenses with Amendments -- 3.1 Does Bx need categorical learning? -- 3.2 Ala-lenses -- 4 Compositionality of ala-lenses -- 4.1 Compositionality of update policies: An example -- 4.2 Sequential composition of ala-lenses -- 4.3 Parallel composition of ala-lenses -- 4.4 Symmetric monoidal structure over ala-lenses -- 4.5 Functoriality of learning in the delta lens setting -- 5 Related work -- 6 Conclusion -- A Appendices -- A.1 Category of parameterized functors pCat -- A.2 Ala-lenses as categorification of ML-learners -- References -- Non-idempotent intersection types in logical form -- Introduction -- 1 Notations and preliminary definitions -- 2 The relational model of the λ-calculus -- 3 The simply typed case -- 3.1 Why do we need another system? -- 3.2 Minimal LJ(I) -- 3.3 Basic properties of LJ(I) -- 3.4 Relation between intersection types and LJ(I) -- 4 The untyped Scott case -- 4.1 Formulas -- 5 Concluding remarks and acknowledgments -- References -- On Computability of Data Word Functions Defined by Transducers -- 1 Introduction -- 2 Data Words and Register Transducers. 2.1 Register Transducers -- 2.2 Technical Properties of Register Automata -- 3 Functionality, Equivalence and Composition of NRT -- 4 Computability and Continuity -- 5 Test-free Register Transducers -- References -- Minimal Coverability Tree Construction Made Complete and Efficient -- 1 Introduction -- 2 Covering abstractions -- 2.1 Petri nets: reachability and covering -- 2.2 Abstraction and acceleration -- 3 A coverability tree algorithm -- 3.1 Specification and illustration -- 3.2 Correctness Proof -- 4 Tool and benchmarks -- 5 Conclusion -- References -- Constructing Infinitary Quotient-Inductive Types -- 1 Introduction -- 2 QW-types -- 3 Quotient-inductive types -- 3.1 General QIT schemas -- 4 Construction of QW-types -- 5 Conclusion -- References -- Relative full completeness for bicategorical cartesian closed structure -- 1 Introduction -- 2 Cartesian closed bicategories -- 2.1 Bicategories -- 2.2 fp-Bicategories -- 2.3 Cartesian closed bicategories -- 3 Bicategorical glueing -- 4 Cartesian closed structure on the glueing bicategory -- 4.1 Finite products in gl(J) -- 4.2 Exponentials in gl(J) -- 5 Relative full completeness -- References -- A duality theoretic view on limits of finite structures -- 1 Introduction -- 2 Preliminaries -- 2.1 Stone-Priestley duality -- 2.2 Stone duality and logic: type spaces -- 2.3 Duality and logic on words -- 3 The space г -- 3.1 The algebraic structure on г -- 3.2 The retraction г → [0, 1] -- 4 Spaces of measures valued in г and in [0, 1] -- 5 The г-valued Stone pairing and limits of finite structures -- 5.1 The г-valued Stone pairing and logic on words -- 5.2 Limits in the spaces of measures -- 6 The logic of measures -- Conclusion -- References -- Correctness of Automatic Differentiation via Diffeologies and Categorical Gluing -- 1 Introduction -- 2 A simple forward-mode AD translation. 3 Semantics of differentiation -- 4 Extending the language: variant and inductive types -- 5 Categorical analysis of forward AD and its correctness -- 6 A continuation-based AD algorithm -- 7 Discussion and future work -- References -- Deep Induction: Induction Rules for (Truly) Nested Types* -- 1 Introduction -- 2 The Key Idea -- 3 Extending to Nested Types -- 4 Theoretical Foundations -- 4.1 Categorical Preliminaries -- 4.2 Syntax and Semantics of ADTs -- 4.3 Induction Rules for ADTs -- 4.4 Syntax and Semantics of Nested Types -- 5 The General Methodology -- 6 Related Work and Directions for Further Investigation -- References -- Exponential Automatic Amortized Resource Analysis* -- 1 Introduction -- 2 Language and Cost Semantics -- 3 Automatic Amortized Resource Analysis -- 4 Exponential Potential -- 5 Mixed Potential -- 6 Exponentials, Polynomials, and Logarithms -- 7 Conclusion and Future Work -- References -- Concurrent Kleene Algebra with Observations: from Hypotheses to Completeness -- 1 Introduction -- 2 Preliminaries -- 3 Pomset contexts -- 4 Concurrent Kleene Algebra with Hypotheses -- 4.1 Reification -- 4.2 Factoring the exchange law -- 4.3 Lifting -- 5 Instantiation to CKA with Observations -- 6 Discussion -- References -- Graded Algebraic Theories -- 1 Introduction -- 2 Preliminaries -- 2.1 Enriched Category Theory -- 2.2 Graded Monads -- 2.3 Day Convolution -- 2.4 Categories Enriched in a Presheaf Category -- 3 Graded Algebraic Theories -- 3.1 Equational Logic -- 3.2 Free Models -- 3.3 Examples -- 4 Graded Lawvere Theories -- 5 Equivalence -- 5.1 Graded Algebraic Theories and Graded Lawvere Theories -- 5.2 Graded Lawvere theories and Finitary Graded Monads -- 6 Combining E ects -- 6.1 Sums -- 6.2 Tensor Products -- 7 Related Work -- 8 Conclusions and Future Work -- References. A Curry-style Semantics of Interaction: From untyped to second-order lazy λμ-calculus. Description based on publisher supplied metadata and other sources. Electronic reproduction. Ann Arbor, Michigan : ProQuest Ebook Central, 2024. Available via World Wide Web. Access may be limited to ProQuest Ebook Central affiliated libraries. Electronic books. König, Barbara. Print version: Goubault-Larrecq, Jean Foundations of Software Science and Computation Structures Cham : Springer International Publishing AG,c2020 9783030452308 ProQuest (Firm) Lecture Notes in Computer Science Series https://ebookcentral.proquest.com/lib/oeawat/detail.action?docID=6702647 Click to View |
language |
English |
format |
eBook |
author |
Goubault-Larrecq, Jean. |
spellingShingle |
Goubault-Larrecq, Jean. Foundations of Software Science and Computation Structures : 23rd International Conference, FOSSACS 2020, Held As Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, April 25-30, 2020, Proceedings. Lecture Notes in Computer Science Series ; Intro -- ETAPS Foreword -- Preface -- Organization -- Contents -- Neural Flocking: MPC-based Supervised Learning of Flocking Controllers -- 1 Introduction -- 2 Background -- 2.1 Model-Predictive Control -- 2.2 Declarative Flocking -- 3 Additional Control Objectives -- 4 Neural Flocking -- 4.1 Training Distributed Flocking Controllers -- 5 Experimental Evaluation -- 5.1 Preliminaries -- 5.2 Results for Basic Flocking -- 5.3 Results for Obstacle and Predator Avoidance -- 5.4 DNC Generalization Results -- 5.5 Statistical Model Checking Results -- 6 Related Work -- 7 Conclusions -- References -- On Well-Founded and Recursive Coalgebras -- 1 Introduction -- 2 Preliminaries -- 2.1 Algebras and Coalgebras. -- 2.2 Preservation Properties. -- 2.3 Factorizations. -- 2.4 Chains. -- 3 Recursive Coalgebras -- 4 The Next Time Operator and Well-Founded Coalgebras -- 5 The General Recursion Theorem and its Converse -- 6 Closure Properties of Well-founded Coalgebras -- 7 Conclusions -- References -- Timed Negotiations* -- 1 Introduction -- 2 Negotiations: Definitions and Brexit example -- 3 Timed Negotiations -- 4 High level view of the main results -- 5 Deterministic Negotiations -- 6 Sound Negotiations -- 7 k-Layered Negotiations -- 7.1 Algorithmic properties -- 7.2 Minimal Execution Time -- 8 Conclusion -- References -- Cartesian Difference Categories -- 1 Introduction -- 2 Cartesian Differential Categories -- 2.1 Cartesian Left Additive Categories -- 2.2 Cartesian Differential Categories -- 3 Change Action Models -- 3.1 Change Actions -- 3.2 Change Action Models -- 4 Cartesian Difference Categories -- 4.1 Infinitesimal Extensions in Left Additive Categories -- 4.2 Cartesian Difference Categories -- 4.3 Another look at Cartesian Differential Categories -- 4.4 Cartesian Difference Categories as Change Action Models -- 4.5 Linear Maps and ε-Linear Maps. 5 Examples of Cartesian Difference Categories -- 5.1 Smooth Functions -- 5.2 Calculus of Finite Diffferences -- 5.3 Module Morphisms -- 5.4 Stream calculus -- 6 Tangent Bundles in Cartesian Di erence Categories -- 6.1 The Tangent Bundle Monad -- 6.2 The Kleisli Category of T -- 7 Conclusions and Future Work -- References -- Contextual Equivalence for Signal Flow Graphs -- 1 Introduction -- 2 Background: the Affine Signal Flow Calculus -- 2.1 Syntax -- 2.2 String Diagrams -- 2.3 Denotational Semantics and Axiomatisation -- 2.4 Affine vs Linear Circuits -- 3 Operational Semantics for Affine Circuits -- 3.1 Trajectories -- 4 Contextual Equivalence and Full Abstraction -- 4.1 From Polynomial Fractions to Trajectories -- 4.2 Proof of Full Abstraction -- 5 Functional Behaviour and Signal Flow Graphs -- 6 Realisability -- 7 Conclusion and Future Work -- References -- Parameterized Synthesis for Fragments of First-Order Logic over Data Words -- 1 Introduction -- 2 Preliminaries -- 3 Parameterized Synthesis Problem -- 4 FO[˘] and Parameterized Vector Games -- 4.1 Satisfiability and Normal Form for FO[˘] -- 4.2 From Synthesis to Parameterized Vector Games -- 5 Results for FO[˘] via Parameterized Vector Games -- 6 Conclusion -- References -- Controlling a random population -- 1 Introduction -- 2 The stochastic control problem -- 3 The sequential ow problem -- 4 Reduction of the stochastic control problem to the sequential flow problem -- 5 Computability of the sequential ow problem -- 6 Conclusions -- Acknowledgements -- References -- Decomposing Probabilistic Lambda-Calculi -- 1 Introduction -- 1.1 Related Work -- 2 The Probabilistic Event λ-Calculus ^PE -- 3 Properties of Permutative Reduction -- 4 Confluence -- 4.1 Parallel Reduction and Permutative Reduction -- 4.2 Complete Reduction -- 5 Strong Normalization for Simply-Typed Terms. 6 Projective Reduction -- 7 Call-by-value Interpretation -- 8 Conclusions and Future Work -- Acknowledgments -- References -- On the k-synchronizability of Systems -- 1 Introduction -- 2 Preliminaries -- 3 k-synchronizable Systems -- 4 Decidability of Reachability for k-synchronizable Systems -- 5 Decidability of k-synchronizability for Mailbox Systems -- 6 k-synchronizability for Peer-to-Peer Systems -- 7 Concluding Remarks and Related works -- References -- General Supervised Learning as Change Propagation with Delta Lenses -- 1 Introduction -- 2 Background: Update propagation and delta lenses -- 2.1 Why deltas. -- 2.2 Consistency restoration via update propagation: An Example -- 2.3 Update propagation and update policies -- 2.4 Delta lenses -- 3 Asymmetric Learning Lenses with Amendments -- 3.1 Does Bx need categorical learning? -- 3.2 Ala-lenses -- 4 Compositionality of ala-lenses -- 4.1 Compositionality of update policies: An example -- 4.2 Sequential composition of ala-lenses -- 4.3 Parallel composition of ala-lenses -- 4.4 Symmetric monoidal structure over ala-lenses -- 4.5 Functoriality of learning in the delta lens setting -- 5 Related work -- 6 Conclusion -- A Appendices -- A.1 Category of parameterized functors pCat -- A.2 Ala-lenses as categorification of ML-learners -- References -- Non-idempotent intersection types in logical form -- Introduction -- 1 Notations and preliminary definitions -- 2 The relational model of the λ-calculus -- 3 The simply typed case -- 3.1 Why do we need another system? -- 3.2 Minimal LJ(I) -- 3.3 Basic properties of LJ(I) -- 3.4 Relation between intersection types and LJ(I) -- 4 The untyped Scott case -- 4.1 Formulas -- 5 Concluding remarks and acknowledgments -- References -- On Computability of Data Word Functions Defined by Transducers -- 1 Introduction -- 2 Data Words and Register Transducers. 2.1 Register Transducers -- 2.2 Technical Properties of Register Automata -- 3 Functionality, Equivalence and Composition of NRT -- 4 Computability and Continuity -- 5 Test-free Register Transducers -- References -- Minimal Coverability Tree Construction Made Complete and Efficient -- 1 Introduction -- 2 Covering abstractions -- 2.1 Petri nets: reachability and covering -- 2.2 Abstraction and acceleration -- 3 A coverability tree algorithm -- 3.1 Specification and illustration -- 3.2 Correctness Proof -- 4 Tool and benchmarks -- 5 Conclusion -- References -- Constructing Infinitary Quotient-Inductive Types -- 1 Introduction -- 2 QW-types -- 3 Quotient-inductive types -- 3.1 General QIT schemas -- 4 Construction of QW-types -- 5 Conclusion -- References -- Relative full completeness for bicategorical cartesian closed structure -- 1 Introduction -- 2 Cartesian closed bicategories -- 2.1 Bicategories -- 2.2 fp-Bicategories -- 2.3 Cartesian closed bicategories -- 3 Bicategorical glueing -- 4 Cartesian closed structure on the glueing bicategory -- 4.1 Finite products in gl(J) -- 4.2 Exponentials in gl(J) -- 5 Relative full completeness -- References -- A duality theoretic view on limits of finite structures -- 1 Introduction -- 2 Preliminaries -- 2.1 Stone-Priestley duality -- 2.2 Stone duality and logic: type spaces -- 2.3 Duality and logic on words -- 3 The space г -- 3.1 The algebraic structure on г -- 3.2 The retraction г → [0, 1] -- 4 Spaces of measures valued in г and in [0, 1] -- 5 The г-valued Stone pairing and limits of finite structures -- 5.1 The г-valued Stone pairing and logic on words -- 5.2 Limits in the spaces of measures -- 6 The logic of measures -- Conclusion -- References -- Correctness of Automatic Differentiation via Diffeologies and Categorical Gluing -- 1 Introduction -- 2 A simple forward-mode AD translation. 3 Semantics of differentiation -- 4 Extending the language: variant and inductive types -- 5 Categorical analysis of forward AD and its correctness -- 6 A continuation-based AD algorithm -- 7 Discussion and future work -- References -- Deep Induction: Induction Rules for (Truly) Nested Types* -- 1 Introduction -- 2 The Key Idea -- 3 Extending to Nested Types -- 4 Theoretical Foundations -- 4.1 Categorical Preliminaries -- 4.2 Syntax and Semantics of ADTs -- 4.3 Induction Rules for ADTs -- 4.4 Syntax and Semantics of Nested Types -- 5 The General Methodology -- 6 Related Work and Directions for Further Investigation -- References -- Exponential Automatic Amortized Resource Analysis* -- 1 Introduction -- 2 Language and Cost Semantics -- 3 Automatic Amortized Resource Analysis -- 4 Exponential Potential -- 5 Mixed Potential -- 6 Exponentials, Polynomials, and Logarithms -- 7 Conclusion and Future Work -- References -- Concurrent Kleene Algebra with Observations: from Hypotheses to Completeness -- 1 Introduction -- 2 Preliminaries -- 3 Pomset contexts -- 4 Concurrent Kleene Algebra with Hypotheses -- 4.1 Reification -- 4.2 Factoring the exchange law -- 4.3 Lifting -- 5 Instantiation to CKA with Observations -- 6 Discussion -- References -- Graded Algebraic Theories -- 1 Introduction -- 2 Preliminaries -- 2.1 Enriched Category Theory -- 2.2 Graded Monads -- 2.3 Day Convolution -- 2.4 Categories Enriched in a Presheaf Category -- 3 Graded Algebraic Theories -- 3.1 Equational Logic -- 3.2 Free Models -- 3.3 Examples -- 4 Graded Lawvere Theories -- 5 Equivalence -- 5.1 Graded Algebraic Theories and Graded Lawvere Theories -- 5.2 Graded Lawvere theories and Finitary Graded Monads -- 6 Combining E ects -- 6.1 Sums -- 6.2 Tensor Products -- 7 Related Work -- 8 Conclusions and Future Work -- References. A Curry-style Semantics of Interaction: From untyped to second-order lazy λμ-calculus. |
author_facet |
Goubault-Larrecq, Jean. König, Barbara. |
author_variant |
j g l jgl |
author2 |
König, Barbara. |
author2_variant |
b k bk |
author2_role |
TeilnehmendeR |
author_sort |
Goubault-Larrecq, Jean. |
title |
Foundations of Software Science and Computation Structures : 23rd International Conference, FOSSACS 2020, Held As Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, April 25-30, 2020, Proceedings. |
title_sub |
23rd International Conference, FOSSACS 2020, Held As Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, April 25-30, 2020, Proceedings. |
title_full |
Foundations of Software Science and Computation Structures : 23rd International Conference, FOSSACS 2020, Held As Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, April 25-30, 2020, Proceedings. |
title_fullStr |
Foundations of Software Science and Computation Structures : 23rd International Conference, FOSSACS 2020, Held As Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, April 25-30, 2020, Proceedings. |
title_full_unstemmed |
Foundations of Software Science and Computation Structures : 23rd International Conference, FOSSACS 2020, Held As Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, April 25-30, 2020, Proceedings. |
title_auth |
Foundations of Software Science and Computation Structures : 23rd International Conference, FOSSACS 2020, Held As Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, April 25-30, 2020, Proceedings. |
title_new |
Foundations of Software Science and Computation Structures : |
title_sort |
foundations of software science and computation structures : 23rd international conference, fossacs 2020, held as part of the european joint conferences on theory and practice of software, etaps 2020, dublin, ireland, april 25-30, 2020, proceedings. |
series |
Lecture Notes in Computer Science Series ; |
series2 |
Lecture Notes in Computer Science Series ; |
publisher |
Springer International Publishing AG, |
publishDate |
2020 |
physical |
1 online resource (657 pages) |
edition |
1st ed. |
contents |
Intro -- ETAPS Foreword -- Preface -- Organization -- Contents -- Neural Flocking: MPC-based Supervised Learning of Flocking Controllers -- 1 Introduction -- 2 Background -- 2.1 Model-Predictive Control -- 2.2 Declarative Flocking -- 3 Additional Control Objectives -- 4 Neural Flocking -- 4.1 Training Distributed Flocking Controllers -- 5 Experimental Evaluation -- 5.1 Preliminaries -- 5.2 Results for Basic Flocking -- 5.3 Results for Obstacle and Predator Avoidance -- 5.4 DNC Generalization Results -- 5.5 Statistical Model Checking Results -- 6 Related Work -- 7 Conclusions -- References -- On Well-Founded and Recursive Coalgebras -- 1 Introduction -- 2 Preliminaries -- 2.1 Algebras and Coalgebras. -- 2.2 Preservation Properties. -- 2.3 Factorizations. -- 2.4 Chains. -- 3 Recursive Coalgebras -- 4 The Next Time Operator and Well-Founded Coalgebras -- 5 The General Recursion Theorem and its Converse -- 6 Closure Properties of Well-founded Coalgebras -- 7 Conclusions -- References -- Timed Negotiations* -- 1 Introduction -- 2 Negotiations: Definitions and Brexit example -- 3 Timed Negotiations -- 4 High level view of the main results -- 5 Deterministic Negotiations -- 6 Sound Negotiations -- 7 k-Layered Negotiations -- 7.1 Algorithmic properties -- 7.2 Minimal Execution Time -- 8 Conclusion -- References -- Cartesian Difference Categories -- 1 Introduction -- 2 Cartesian Differential Categories -- 2.1 Cartesian Left Additive Categories -- 2.2 Cartesian Differential Categories -- 3 Change Action Models -- 3.1 Change Actions -- 3.2 Change Action Models -- 4 Cartesian Difference Categories -- 4.1 Infinitesimal Extensions in Left Additive Categories -- 4.2 Cartesian Difference Categories -- 4.3 Another look at Cartesian Differential Categories -- 4.4 Cartesian Difference Categories as Change Action Models -- 4.5 Linear Maps and ε-Linear Maps. 5 Examples of Cartesian Difference Categories -- 5.1 Smooth Functions -- 5.2 Calculus of Finite Diffferences -- 5.3 Module Morphisms -- 5.4 Stream calculus -- 6 Tangent Bundles in Cartesian Di erence Categories -- 6.1 The Tangent Bundle Monad -- 6.2 The Kleisli Category of T -- 7 Conclusions and Future Work -- References -- Contextual Equivalence for Signal Flow Graphs -- 1 Introduction -- 2 Background: the Affine Signal Flow Calculus -- 2.1 Syntax -- 2.2 String Diagrams -- 2.3 Denotational Semantics and Axiomatisation -- 2.4 Affine vs Linear Circuits -- 3 Operational Semantics for Affine Circuits -- 3.1 Trajectories -- 4 Contextual Equivalence and Full Abstraction -- 4.1 From Polynomial Fractions to Trajectories -- 4.2 Proof of Full Abstraction -- 5 Functional Behaviour and Signal Flow Graphs -- 6 Realisability -- 7 Conclusion and Future Work -- References -- Parameterized Synthesis for Fragments of First-Order Logic over Data Words -- 1 Introduction -- 2 Preliminaries -- 3 Parameterized Synthesis Problem -- 4 FO[˘] and Parameterized Vector Games -- 4.1 Satisfiability and Normal Form for FO[˘] -- 4.2 From Synthesis to Parameterized Vector Games -- 5 Results for FO[˘] via Parameterized Vector Games -- 6 Conclusion -- References -- Controlling a random population -- 1 Introduction -- 2 The stochastic control problem -- 3 The sequential ow problem -- 4 Reduction of the stochastic control problem to the sequential flow problem -- 5 Computability of the sequential ow problem -- 6 Conclusions -- Acknowledgements -- References -- Decomposing Probabilistic Lambda-Calculi -- 1 Introduction -- 1.1 Related Work -- 2 The Probabilistic Event λ-Calculus ^PE -- 3 Properties of Permutative Reduction -- 4 Confluence -- 4.1 Parallel Reduction and Permutative Reduction -- 4.2 Complete Reduction -- 5 Strong Normalization for Simply-Typed Terms. 6 Projective Reduction -- 7 Call-by-value Interpretation -- 8 Conclusions and Future Work -- Acknowledgments -- References -- On the k-synchronizability of Systems -- 1 Introduction -- 2 Preliminaries -- 3 k-synchronizable Systems -- 4 Decidability of Reachability for k-synchronizable Systems -- 5 Decidability of k-synchronizability for Mailbox Systems -- 6 k-synchronizability for Peer-to-Peer Systems -- 7 Concluding Remarks and Related works -- References -- General Supervised Learning as Change Propagation with Delta Lenses -- 1 Introduction -- 2 Background: Update propagation and delta lenses -- 2.1 Why deltas. -- 2.2 Consistency restoration via update propagation: An Example -- 2.3 Update propagation and update policies -- 2.4 Delta lenses -- 3 Asymmetric Learning Lenses with Amendments -- 3.1 Does Bx need categorical learning? -- 3.2 Ala-lenses -- 4 Compositionality of ala-lenses -- 4.1 Compositionality of update policies: An example -- 4.2 Sequential composition of ala-lenses -- 4.3 Parallel composition of ala-lenses -- 4.4 Symmetric monoidal structure over ala-lenses -- 4.5 Functoriality of learning in the delta lens setting -- 5 Related work -- 6 Conclusion -- A Appendices -- A.1 Category of parameterized functors pCat -- A.2 Ala-lenses as categorification of ML-learners -- References -- Non-idempotent intersection types in logical form -- Introduction -- 1 Notations and preliminary definitions -- 2 The relational model of the λ-calculus -- 3 The simply typed case -- 3.1 Why do we need another system? -- 3.2 Minimal LJ(I) -- 3.3 Basic properties of LJ(I) -- 3.4 Relation between intersection types and LJ(I) -- 4 The untyped Scott case -- 4.1 Formulas -- 5 Concluding remarks and acknowledgments -- References -- On Computability of Data Word Functions Defined by Transducers -- 1 Introduction -- 2 Data Words and Register Transducers. 2.1 Register Transducers -- 2.2 Technical Properties of Register Automata -- 3 Functionality, Equivalence and Composition of NRT -- 4 Computability and Continuity -- 5 Test-free Register Transducers -- References -- Minimal Coverability Tree Construction Made Complete and Efficient -- 1 Introduction -- 2 Covering abstractions -- 2.1 Petri nets: reachability and covering -- 2.2 Abstraction and acceleration -- 3 A coverability tree algorithm -- 3.1 Specification and illustration -- 3.2 Correctness Proof -- 4 Tool and benchmarks -- 5 Conclusion -- References -- Constructing Infinitary Quotient-Inductive Types -- 1 Introduction -- 2 QW-types -- 3 Quotient-inductive types -- 3.1 General QIT schemas -- 4 Construction of QW-types -- 5 Conclusion -- References -- Relative full completeness for bicategorical cartesian closed structure -- 1 Introduction -- 2 Cartesian closed bicategories -- 2.1 Bicategories -- 2.2 fp-Bicategories -- 2.3 Cartesian closed bicategories -- 3 Bicategorical glueing -- 4 Cartesian closed structure on the glueing bicategory -- 4.1 Finite products in gl(J) -- 4.2 Exponentials in gl(J) -- 5 Relative full completeness -- References -- A duality theoretic view on limits of finite structures -- 1 Introduction -- 2 Preliminaries -- 2.1 Stone-Priestley duality -- 2.2 Stone duality and logic: type spaces -- 2.3 Duality and logic on words -- 3 The space г -- 3.1 The algebraic structure on г -- 3.2 The retraction г → [0, 1] -- 4 Spaces of measures valued in г and in [0, 1] -- 5 The г-valued Stone pairing and limits of finite structures -- 5.1 The г-valued Stone pairing and logic on words -- 5.2 Limits in the spaces of measures -- 6 The logic of measures -- Conclusion -- References -- Correctness of Automatic Differentiation via Diffeologies and Categorical Gluing -- 1 Introduction -- 2 A simple forward-mode AD translation. 3 Semantics of differentiation -- 4 Extending the language: variant and inductive types -- 5 Categorical analysis of forward AD and its correctness -- 6 A continuation-based AD algorithm -- 7 Discussion and future work -- References -- Deep Induction: Induction Rules for (Truly) Nested Types* -- 1 Introduction -- 2 The Key Idea -- 3 Extending to Nested Types -- 4 Theoretical Foundations -- 4.1 Categorical Preliminaries -- 4.2 Syntax and Semantics of ADTs -- 4.3 Induction Rules for ADTs -- 4.4 Syntax and Semantics of Nested Types -- 5 The General Methodology -- 6 Related Work and Directions for Further Investigation -- References -- Exponential Automatic Amortized Resource Analysis* -- 1 Introduction -- 2 Language and Cost Semantics -- 3 Automatic Amortized Resource Analysis -- 4 Exponential Potential -- 5 Mixed Potential -- 6 Exponentials, Polynomials, and Logarithms -- 7 Conclusion and Future Work -- References -- Concurrent Kleene Algebra with Observations: from Hypotheses to Completeness -- 1 Introduction -- 2 Preliminaries -- 3 Pomset contexts -- 4 Concurrent Kleene Algebra with Hypotheses -- 4.1 Reification -- 4.2 Factoring the exchange law -- 4.3 Lifting -- 5 Instantiation to CKA with Observations -- 6 Discussion -- References -- Graded Algebraic Theories -- 1 Introduction -- 2 Preliminaries -- 2.1 Enriched Category Theory -- 2.2 Graded Monads -- 2.3 Day Convolution -- 2.4 Categories Enriched in a Presheaf Category -- 3 Graded Algebraic Theories -- 3.1 Equational Logic -- 3.2 Free Models -- 3.3 Examples -- 4 Graded Lawvere Theories -- 5 Equivalence -- 5.1 Graded Algebraic Theories and Graded Lawvere Theories -- 5.2 Graded Lawvere theories and Finitary Graded Monads -- 6 Combining E ects -- 6.1 Sums -- 6.2 Tensor Products -- 7 Related Work -- 8 Conclusions and Future Work -- References. A Curry-style Semantics of Interaction: From untyped to second-order lazy λμ-calculus. |
isbn |
9783030452315 9783030452308 |
callnumber-first |
Q - Science |
callnumber-subject |
QA - Mathematics |
callnumber-label |
QA8 |
callnumber-sort |
QA 18.9 210.3 |
genre |
Electronic books. |
genre_facet |
Electronic books. |
url |
https://ebookcentral.proquest.com/lib/oeawat/detail.action?docID=6702647 |
illustrated |
Not Illustrated |
oclc_num |
1239981377 |
work_keys_str_mv |
AT goubaultlarrecqjean foundationsofsoftwarescienceandcomputationstructures23rdinternationalconferencefossacs2020heldaspartoftheeuropeanjointconferencesontheoryandpracticeofsoftwareetaps2020dublinirelandapril25302020proceedings AT konigbarbara foundationsofsoftwarescienceandcomputationstructures23rdinternationalconferencefossacs2020heldaspartoftheeuropeanjointconferencesontheoryandpracticeofsoftwareetaps2020dublinirelandapril25302020proceedings |
status_str |
n |
ids_txt_mv |
(MiAaPQ)5006702647 (Au-PeEL)EBL6702647 (OCoLC)1239981377 |
carrierType_str_mv |
cr |
hierarchy_parent_title |
Lecture Notes in Computer Science Series ; v.12077 |
is_hierarchy_title |
Foundations of Software Science and Computation Structures : 23rd International Conference, FOSSACS 2020, Held As Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, April 25-30, 2020, Proceedings. |
container_title |
Lecture Notes in Computer Science Series ; v.12077 |
author2_original_writing_str_mv |
noLinkedField |
_version_ |
1792331059412598784 |
fullrecord |
<?xml version="1.0" encoding="UTF-8"?><collection xmlns="http://www.loc.gov/MARC21/slim"><record><leader>11413nam a22004693i 4500</leader><controlfield tag="001">5006702647</controlfield><controlfield tag="003">MiAaPQ</controlfield><controlfield tag="005">20240229073843.0</controlfield><controlfield tag="006">m o d | </controlfield><controlfield tag="007">cr cnu||||||||</controlfield><controlfield tag="008">240229s2020 xx o ||||0 eng d</controlfield><datafield tag="020" ind1=" " ind2=" "><subfield code="a">9783030452315</subfield><subfield code="q">(electronic bk.)</subfield></datafield><datafield tag="020" ind1=" " ind2=" "><subfield code="z">9783030452308</subfield></datafield><datafield tag="035" ind1=" " ind2=" "><subfield code="a">(MiAaPQ)5006702647</subfield></datafield><datafield tag="035" ind1=" " ind2=" "><subfield code="a">(Au-PeEL)EBL6702647</subfield></datafield><datafield tag="035" ind1=" " ind2=" "><subfield code="a">(OCoLC)1239981377</subfield></datafield><datafield tag="040" ind1=" " ind2=" "><subfield code="a">MiAaPQ</subfield><subfield code="b">eng</subfield><subfield code="e">rda</subfield><subfield code="e">pn</subfield><subfield code="c">MiAaPQ</subfield><subfield code="d">MiAaPQ</subfield></datafield><datafield tag="050" ind1=" " ind2="4"><subfield code="a">QA8.9-10.3</subfield></datafield><datafield tag="100" ind1="1" ind2=" "><subfield code="a">Goubault-Larrecq, Jean.</subfield></datafield><datafield tag="245" ind1="1" ind2="0"><subfield code="a">Foundations of Software Science and Computation Structures :</subfield><subfield code="b">23rd International Conference, FOSSACS 2020, Held As Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, April 25-30, 2020, Proceedings.</subfield></datafield><datafield tag="250" ind1=" " ind2=" "><subfield code="a">1st ed.</subfield></datafield><datafield tag="264" ind1=" " ind2="1"><subfield code="a">Cham :</subfield><subfield code="b">Springer International Publishing AG,</subfield><subfield code="c">2020.</subfield></datafield><datafield tag="264" ind1=" " ind2="4"><subfield code="c">©2020.</subfield></datafield><datafield tag="300" ind1=" " ind2=" "><subfield code="a">1 online resource (657 pages)</subfield></datafield><datafield tag="336" ind1=" " ind2=" "><subfield code="a">text</subfield><subfield code="b">txt</subfield><subfield code="2">rdacontent</subfield></datafield><datafield tag="337" ind1=" " ind2=" "><subfield code="a">computer</subfield><subfield code="b">c</subfield><subfield code="2">rdamedia</subfield></datafield><datafield tag="338" ind1=" " ind2=" "><subfield code="a">online resource</subfield><subfield code="b">cr</subfield><subfield code="2">rdacarrier</subfield></datafield><datafield tag="490" ind1="1" ind2=" "><subfield code="a">Lecture Notes in Computer Science Series ;</subfield><subfield code="v">v.12077</subfield></datafield><datafield tag="505" ind1="0" ind2=" "><subfield code="a">Intro -- ETAPS Foreword -- Preface -- Organization -- Contents -- Neural Flocking: MPC-based Supervised Learning of Flocking Controllers -- 1 Introduction -- 2 Background -- 2.1 Model-Predictive Control -- 2.2 Declarative Flocking -- 3 Additional Control Objectives -- 4 Neural Flocking -- 4.1 Training Distributed Flocking Controllers -- 5 Experimental Evaluation -- 5.1 Preliminaries -- 5.2 Results for Basic Flocking -- 5.3 Results for Obstacle and Predator Avoidance -- 5.4 DNC Generalization Results -- 5.5 Statistical Model Checking Results -- 6 Related Work -- 7 Conclusions -- References -- On Well-Founded and Recursive Coalgebras -- 1 Introduction -- 2 Preliminaries -- 2.1 Algebras and Coalgebras. -- 2.2 Preservation Properties. -- 2.3 Factorizations. -- 2.4 Chains. -- 3 Recursive Coalgebras -- 4 The Next Time Operator and Well-Founded Coalgebras -- 5 The General Recursion Theorem and its Converse -- 6 Closure Properties of Well-founded Coalgebras -- 7 Conclusions -- References -- Timed Negotiations* -- 1 Introduction -- 2 Negotiations: Definitions and Brexit example -- 3 Timed Negotiations -- 4 High level view of the main results -- 5 Deterministic Negotiations -- 6 Sound Negotiations -- 7 k-Layered Negotiations -- 7.1 Algorithmic properties -- 7.2 Minimal Execution Time -- 8 Conclusion -- References -- Cartesian Difference Categories -- 1 Introduction -- 2 Cartesian Differential Categories -- 2.1 Cartesian Left Additive Categories -- 2.2 Cartesian Differential Categories -- 3 Change Action Models -- 3.1 Change Actions -- 3.2 Change Action Models -- 4 Cartesian Difference Categories -- 4.1 Infinitesimal Extensions in Left Additive Categories -- 4.2 Cartesian Difference Categories -- 4.3 Another look at Cartesian Differential Categories -- 4.4 Cartesian Difference Categories as Change Action Models -- 4.5 Linear Maps and ε-Linear Maps.</subfield></datafield><datafield tag="505" ind1="8" ind2=" "><subfield code="a">5 Examples of Cartesian Difference Categories -- 5.1 Smooth Functions -- 5.2 Calculus of Finite Diffferences -- 5.3 Module Morphisms -- 5.4 Stream calculus -- 6 Tangent Bundles in Cartesian Di erence Categories -- 6.1 The Tangent Bundle Monad -- 6.2 The Kleisli Category of T -- 7 Conclusions and Future Work -- References -- Contextual Equivalence for Signal Flow Graphs -- 1 Introduction -- 2 Background: the Affine Signal Flow Calculus -- 2.1 Syntax -- 2.2 String Diagrams -- 2.3 Denotational Semantics and Axiomatisation -- 2.4 Affine vs Linear Circuits -- 3 Operational Semantics for Affine Circuits -- 3.1 Trajectories -- 4 Contextual Equivalence and Full Abstraction -- 4.1 From Polynomial Fractions to Trajectories -- 4.2 Proof of Full Abstraction -- 5 Functional Behaviour and Signal Flow Graphs -- 6 Realisability -- 7 Conclusion and Future Work -- References -- Parameterized Synthesis for Fragments of First-Order Logic over Data Words -- 1 Introduction -- 2 Preliminaries -- 3 Parameterized Synthesis Problem -- 4 FO[˘] and Parameterized Vector Games -- 4.1 Satisfiability and Normal Form for FO[˘] -- 4.2 From Synthesis to Parameterized Vector Games -- 5 Results for FO[˘] via Parameterized Vector Games -- 6 Conclusion -- References -- Controlling a random population -- 1 Introduction -- 2 The stochastic control problem -- 3 The sequential ow problem -- 4 Reduction of the stochastic control problem to the sequential flow problem -- 5 Computability of the sequential ow problem -- 6 Conclusions -- Acknowledgements -- References -- Decomposing Probabilistic Lambda-Calculi -- 1 Introduction -- 1.1 Related Work -- 2 The Probabilistic Event λ-Calculus ^PE -- 3 Properties of Permutative Reduction -- 4 Confluence -- 4.1 Parallel Reduction and Permutative Reduction -- 4.2 Complete Reduction -- 5 Strong Normalization for Simply-Typed Terms.</subfield></datafield><datafield tag="505" ind1="8" ind2=" "><subfield code="a">6 Projective Reduction -- 7 Call-by-value Interpretation -- 8 Conclusions and Future Work -- Acknowledgments -- References -- On the k-synchronizability of Systems -- 1 Introduction -- 2 Preliminaries -- 3 k-synchronizable Systems -- 4 Decidability of Reachability for k-synchronizable Systems -- 5 Decidability of k-synchronizability for Mailbox Systems -- 6 k-synchronizability for Peer-to-Peer Systems -- 7 Concluding Remarks and Related works -- References -- General Supervised Learning as Change Propagation with Delta Lenses -- 1 Introduction -- 2 Background: Update propagation and delta lenses -- 2.1 Why deltas. -- 2.2 Consistency restoration via update propagation: An Example -- 2.3 Update propagation and update policies -- 2.4 Delta lenses -- 3 Asymmetric Learning Lenses with Amendments -- 3.1 Does Bx need categorical learning? -- 3.2 Ala-lenses -- 4 Compositionality of ala-lenses -- 4.1 Compositionality of update policies: An example -- 4.2 Sequential composition of ala-lenses -- 4.3 Parallel composition of ala-lenses -- 4.4 Symmetric monoidal structure over ala-lenses -- 4.5 Functoriality of learning in the delta lens setting -- 5 Related work -- 6 Conclusion -- A Appendices -- A.1 Category of parameterized functors pCat -- A.2 Ala-lenses as categorification of ML-learners -- References -- Non-idempotent intersection types in logical form -- Introduction -- 1 Notations and preliminary definitions -- 2 The relational model of the λ-calculus -- 3 The simply typed case -- 3.1 Why do we need another system? -- 3.2 Minimal LJ(I) -- 3.3 Basic properties of LJ(I) -- 3.4 Relation between intersection types and LJ(I) -- 4 The untyped Scott case -- 4.1 Formulas -- 5 Concluding remarks and acknowledgments -- References -- On Computability of Data Word Functions Defined by Transducers -- 1 Introduction -- 2 Data Words and Register Transducers.</subfield></datafield><datafield tag="505" ind1="8" ind2=" "><subfield code="a">2.1 Register Transducers -- 2.2 Technical Properties of Register Automata -- 3 Functionality, Equivalence and Composition of NRT -- 4 Computability and Continuity -- 5 Test-free Register Transducers -- References -- Minimal Coverability Tree Construction Made Complete and Efficient -- 1 Introduction -- 2 Covering abstractions -- 2.1 Petri nets: reachability and covering -- 2.2 Abstraction and acceleration -- 3 A coverability tree algorithm -- 3.1 Specification and illustration -- 3.2 Correctness Proof -- 4 Tool and benchmarks -- 5 Conclusion -- References -- Constructing Infinitary Quotient-Inductive Types -- 1 Introduction -- 2 QW-types -- 3 Quotient-inductive types -- 3.1 General QIT schemas -- 4 Construction of QW-types -- 5 Conclusion -- References -- Relative full completeness for bicategorical cartesian closed structure -- 1 Introduction -- 2 Cartesian closed bicategories -- 2.1 Bicategories -- 2.2 fp-Bicategories -- 2.3 Cartesian closed bicategories -- 3 Bicategorical glueing -- 4 Cartesian closed structure on the glueing bicategory -- 4.1 Finite products in gl(J) -- 4.2 Exponentials in gl(J) -- 5 Relative full completeness -- References -- A duality theoretic view on limits of finite structures -- 1 Introduction -- 2 Preliminaries -- 2.1 Stone-Priestley duality -- 2.2 Stone duality and logic: type spaces -- 2.3 Duality and logic on words -- 3 The space г -- 3.1 The algebraic structure on г -- 3.2 The retraction г → [0, 1] -- 4 Spaces of measures valued in г and in [0, 1] -- 5 The г-valued Stone pairing and limits of finite structures -- 5.1 The г-valued Stone pairing and logic on words -- 5.2 Limits in the spaces of measures -- 6 The logic of measures -- Conclusion -- References -- Correctness of Automatic Differentiation via Diffeologies and Categorical Gluing -- 1 Introduction -- 2 A simple forward-mode AD translation.</subfield></datafield><datafield tag="505" ind1="8" ind2=" "><subfield code="a">3 Semantics of differentiation -- 4 Extending the language: variant and inductive types -- 5 Categorical analysis of forward AD and its correctness -- 6 A continuation-based AD algorithm -- 7 Discussion and future work -- References -- Deep Induction: Induction Rules for (Truly) Nested Types* -- 1 Introduction -- 2 The Key Idea -- 3 Extending to Nested Types -- 4 Theoretical Foundations -- 4.1 Categorical Preliminaries -- 4.2 Syntax and Semantics of ADTs -- 4.3 Induction Rules for ADTs -- 4.4 Syntax and Semantics of Nested Types -- 5 The General Methodology -- 6 Related Work and Directions for Further Investigation -- References -- Exponential Automatic Amortized Resource Analysis* -- 1 Introduction -- 2 Language and Cost Semantics -- 3 Automatic Amortized Resource Analysis -- 4 Exponential Potential -- 5 Mixed Potential -- 6 Exponentials, Polynomials, and Logarithms -- 7 Conclusion and Future Work -- References -- Concurrent Kleene Algebra with Observations: from Hypotheses to Completeness -- 1 Introduction -- 2 Preliminaries -- 3 Pomset contexts -- 4 Concurrent Kleene Algebra with Hypotheses -- 4.1 Reification -- 4.2 Factoring the exchange law -- 4.3 Lifting -- 5 Instantiation to CKA with Observations -- 6 Discussion -- References -- Graded Algebraic Theories -- 1 Introduction -- 2 Preliminaries -- 2.1 Enriched Category Theory -- 2.2 Graded Monads -- 2.3 Day Convolution -- 2.4 Categories Enriched in a Presheaf Category -- 3 Graded Algebraic Theories -- 3.1 Equational Logic -- 3.2 Free Models -- 3.3 Examples -- 4 Graded Lawvere Theories -- 5 Equivalence -- 5.1 Graded Algebraic Theories and Graded Lawvere Theories -- 5.2 Graded Lawvere theories and Finitary Graded Monads -- 6 Combining E ects -- 6.1 Sums -- 6.2 Tensor Products -- 7 Related Work -- 8 Conclusions and Future Work -- References.</subfield></datafield><datafield tag="505" ind1="8" ind2=" "><subfield code="a">A Curry-style Semantics of Interaction: From untyped to second-order lazy λμ-calculus.</subfield></datafield><datafield tag="588" ind1=" " ind2=" "><subfield code="a">Description based on publisher supplied metadata and other sources.</subfield></datafield><datafield tag="590" ind1=" " ind2=" "><subfield code="a">Electronic reproduction. Ann Arbor, Michigan : ProQuest Ebook Central, 2024. Available via World Wide Web. Access may be limited to ProQuest Ebook Central affiliated libraries. </subfield></datafield><datafield tag="655" ind1=" " ind2="4"><subfield code="a">Electronic books.</subfield></datafield><datafield tag="700" ind1="1" ind2=" "><subfield code="a">König, Barbara.</subfield></datafield><datafield tag="776" ind1="0" ind2="8"><subfield code="i">Print version:</subfield><subfield code="a">Goubault-Larrecq, Jean</subfield><subfield code="t">Foundations of Software Science and Computation Structures</subfield><subfield code="d">Cham : Springer International Publishing AG,c2020</subfield><subfield code="z">9783030452308</subfield></datafield><datafield tag="797" ind1="2" ind2=" "><subfield code="a">ProQuest (Firm)</subfield></datafield><datafield tag="830" ind1=" " ind2="0"><subfield code="a">Lecture Notes in Computer Science Series</subfield></datafield><datafield tag="856" ind1="4" ind2="0"><subfield code="u">https://ebookcentral.proquest.com/lib/oeawat/detail.action?docID=6702647</subfield><subfield code="z">Click to View</subfield></datafield></record></collection> |