{"text_format":"2","workbook":"xls","n_sheets":1,"sheets":["report2"],"not_rendered":{"charts":0,"images":0,"macros":0,"external_links":1,"defined_names":1,"comments":0,"pivot_tables":0},"unopened":[],"bounds":{"document_bytes":16777216,"sheet_cells":100000,"run_cost":"one","rows_first":2000,"rows_last":500,"rows_between":2000,"halvings":0,"cell_chars":16384,"cell_head_chars":4096},"cells_cut":0,"cells_raw":0,"read":"whole","date_system":"1900","formulas":"cached_only"}

{"sheet":"report2","index":0,"n_rows":19,"n_cols":5,"rows_kept":19,"cut":false,"hidden":false,"merged":[[0,2,0,3],[0,4,0,5],[1,2,1,3],[1,4,1,5],[2,2,2,3],[4,2,4,3],[5,2,5,3],[6,2,6,3],[7,2,7,3],[8,2,8,3],[10,2,10,3],[11,2,11,3],[14,2,14,3]],"flags":["formulas_cached_only"]}
[null,"1.","Record Nr.",null,"UNISA996490353403316"]
[null,null,"Titolo",null,"Mathematics of program construction : 14th International Conference, MPC 2022, Tbilisi, Georgia, September 26-28, 2022, proceedings / / edited by Ekaterina Komendantskaya"]
[null,null,"Pubbl/distr/stampa",null,"Cham, Switzerland : , : Springer, , [2022]"]
[{"$nulls":4},"©2022"]
[null,null,"ISBN",null,"3-031-16912-3"]
[null,null,"Descrizione fisica",null,"1 online resource (281 pages)"]
[null,null,"Collana",null,"Lecture Notes in Computer Science ; ; v.13544"]
[null,null,"Disciplina",null,"371.39445"]
[null,null,"Soggetti",null,"Computer programming"]
[{"$nulls":4},"Computer science - Mathematics"]
[null,null,"Lingua di pubblicazione",null,"Inglese"]
[null,null,"Formato",null,"Materiale a stampa"]
[null,null,null,"Livello bibliografico","Monografia"]
[null,null,null,"Note generali","Includes index."]
[null,null,"Nota di contenuto",null,"Intro -- Preface -- Organization -- Abstracts of Invited Talks -- Picking Your Way Through Pascal's Triangle -- The Semifree Monad -- Lens Theoretic Foundations for Learning: From Semantics to Verification -- Contents -- Breadth-First Traversal via Staging -- 1 Introduction -- 2 Applicative Functors -- 2.1 Applicative Traversal -- 2.2 Trees -- 3 Shape, Contents, Relabelling -- 4 Fusing Traversals via Staged Computation -- 4.1 The Repmin Problem -- 4.2 Fusing Traversals -- 4.3 Day Convolution -- 4.4 Repmin in Two Phases -- 5 Multiple Phases -- 5.1 Free Applicatives -- 5.2 Two Phases, More or Less -- 5.3 The `Sort-Tree' Problem -- 6 Breadth-first Traversal in Stages -- 7 Discussion -- A Fusion of traversals -- A.1 Length-indexed vectors -- A.2 Size-indexed trees -- A.3 Make functions -- A.4 Representation Theorem -- A.5 Commutativity -- References -- Subtyping Without Reduction -- 1 Introduction -- 2 Example: Even Numbers -- 3 Path Types -- 4 Higher-Inductive Evenness -- 5 Higher-Inductive Recursive Even Numbers -- 6 Reflection -- 7 Example: Ordered Finite Sets -- 8 IF Formalisation -- 8.1 Indexed Containers -- 8.2 Propositional Monads -- 8.3 Free Propositional Monad -- 8.4 Example -- 9 IR Formalisation -- 9.1 Fibers -- 9.2 Free Subtype Extension -- 9.3 Decode Is an Embedding -- 9.4 Equivalence Between IF and IR Approaches -- 9.5 Example -- 10 Generalising Our Technique -- 11 Related Approaches -- 12 Conclusion -- References -- Calculating Datastructures -- 1 Introduction -- 2 One-sided Flexible "]
[{"$nulls":4},"Arrays -- 3 Peano Numerals -- 3.1 Number Type -- 3.2 Index Type -- 4 Functions as Datastructures -- 5 Lists Also Known as Vectors -- 6 Leibniz Numerals -- 6.1 Number Type -- 6.2 Index Type -- 7 Functions as Datastructures, Revisited -- 8 One-two Trees -- 9 Braun Trees -- 9.1 Index Type, Revisited -- 9.2 Trie Type, Revisited -- 10 Random-Access Lists."]
[{"$nulls":4},"11 Related Work -- 12 Conclusion -- A  Deriving Operations -- References -- Flexibly Graded Monads and Graded Algebras -- 1 Introduction -- 2 Graded Monads -- 2.1 Examples -- 3 Locally Graded Categories -- 4 Flexibly and Rigidly Graded Monads -- 4.1 Eilenberg-Moore and Kleisli -- 4.2 E-actegories -- 5 Rigidly Graded Monads from Flexibly Graded Monads -- 6 Flexibly Graded Monads from Rigidly Graded Monads -- 6.1 Constructing Extensions -- 7 Related Work -- 8 Conclusions -- References -- Folding over Neural Networks -- 1 Introduction -- 2 Background -- 3 Fully Connected Networks -- 3.1 Forward Propagation as a Catamorphism -- 3.2 Back Propagation as an Anamorphism -- 3.3 Training Neural Networks with Metamorphisms -- 4 Neural Networks à la Carte -- 4.1 Free Monads and Coproducts -- 4.2 Training Neural Networks with Free Monads -- 5 Training with Just Folds -- 5.1 Back Propagation as a Fold -- 5.2 Training as a Single Fold -- 5.3 Example: Training a Fully Connected Network -- 6 Summary -- 6.1 Related Work -- References -- Towards a Practical Library for Monadic Equational Reasoning in Coq -- 1 Introduction -- 2 An Extensible Implementation of Monad Interfaces -- 2.1 Hierarchy-Builder in a nutshell -- 2.2 Functors and Natural Transformations -- 2.3 Formalization of Monads -- 2.4 Extending the Hierarchy with New Monad Interfaces -- 2.5 Monad Transformers Using Hierarchy-Builder -- 3 Difficulties with the Termination of Monadic Functions -- 3.1 Background: Standard Coq Tooling to Prove Termination -- 3.2 Limitations of Coq Standard Tooling to Prove Termination -- 4 Add Dependent Types to Return Types for Formal Proofs -- 4.1 Add Dependent Types to Called Functions to Prove Termination -- 4.2 Add Dependent Types with a Dependently-Typed Assertion -- 5 A Complete Formalization of Quicksort Derivation -- 5.1 Formal Properties of Nondeterministic Permutations."]
[{"$nulls":4},"5.2 Program Refinement -- 5.3 A Complete Formalization of Functional Quicksort -- 5.4 A Complete Formalization of In-Place Quicksort -- 6 Related Work -- 7 Conclusion -- References -- Semantic Preservation for a Type Directed Translation Scheme of Featherweight Go -- 1 Introduction -- 2 Overview -- 3 Featherweight Go -- 4 Type Directed Translation -- 4.1 Target Language -- 4.2 Translation -- 5 Semantic Preservation -- 6 Related Work -- 7 Conclusion -- References -- Streams of Approximations, Equivalence of Recursive Effectful Programs -- 1 Introduction -- 2 Recursion Streams -- 2.1 Approximations -- 2.2 Relating Streams -- 3 Higher-Order Programs -- 3.1 Algebraic Effect Operations -- 3.2 Call-by-Push-Value -- 4 Effectful Behaviour -- 4.1 Improvement Orders -- 5 Full Program Denotations and Equivalence -- 5.1 The Subtlety of Approximation -- 5.2 The Substitution Lemma -- 5.3 Operational Semantics and Soundness -- 6 Discussion and Conclusion -- References -- Fantastic Morphisms and Wherepg to Find Them -- 1 Introduction -- 1.1 Diversification -- 1.2 Unification -- 1.3 Overview -- 2 Datatypes and Fixed Points -- 3 Fundamental Recursion Schemes -- 3.1 Catamorphisms -- 3.2 Anamorphisms -- 3.3 Hylomorphisms -- 4 Accumulations -- 5 Mutual Recursion -- 5.1 Mutumorphisms -- 5.2 Dual of Mutumorphisms -- 6 Primitive (Co)Recursion -- 6.1 Paramorphisms -- 6.2 Apomorphisms -- 6.3 Zygomorphisms -- 7 Course-of-Value (Co)Recursion -- 7.1 Histomorphisms -- 7.2 "]
[{"$nulls":4},"Dynamorphisms -- 7.3 Futumorphisms -- 8 Monadic Structural Recursion -- 8.1 Monadic Catamorphism -- 8.2 More Monadic Recursion Schemes -- 9 Structural Recursion on gadts -- 10 Equational Reasoning with Recursion Schemes -- 11 Closing Remarks and Further Reading -- References -- Author Index."]