Practical Aspects of Declarative Languages : 26th International Symposium, PADL 2024, London, UK, January 15-16, 2024, Proceedings / / Martin Gebser and Ilya Sergey, editors |
Edizione | [First edition.] |
Pubbl/distr/stampa | Cham, Switzerland : , : Springer, , [2023] |
Descrizione fisica | 1 online resource (238 pages) |
Disciplina | 005.131 |
Collana | Lecture Notes in Computer Science Series |
Soggetto topico |
Declarative programming
Declarative programming languages |
ISBN | 3-031-52038-6 |
Formato | Materiale a stampa |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | Invited Talks -- Whats and Whys of Neural Network Verification (A Declarative Programming Perspective) -- Modular Higher-Order Effects -- Regular Papers -- Forget and Regeneration Techniques for Optimizing ASP-based Stream Reasoning -- Asynchronous Reactive Programming with Modal Types in Haskell -- FOLD-SE: An Efficient Rule-based Machine Learning Algorithm with Scalable Explainability -- Marketplace Logistics via Answer Set Programming -- Rhyme: A Data-Centric Expressive Query Language for Nested Data Structures -- Rethinking Answer Set Programming Templates -- Cutting the Cake Into Crumbs: Verifying Envy-Free Cake-Cutting Protocols using Bounded Integer Arithmetic -- A direct ASP Encoding for Declare -- Using Logic Programming and Kernel-Grouping for Improving Interpretability of Convolutional Neural Networks -- Hardware implementation of OCaml using a synchronous functional language -- Ontological Reasoning over Shy and Warded Datalog+/- for Streaming-based Architectures -- Explanation and Knowledge Acquisition in Ad Hoc Teamwork -- Automated Interactive Domain-Specific Conversational Agents that Understand Human Dialogs. |
Record Nr. | UNINA-9910800112503321 |
Cham, Switzerland : , : Springer, , [2023] | ||
Materiale a stampa | ||
Lo trovi qui: Univ. Federico II | ||
|
Practical Aspects of Declarative Languages : 26th International Symposium, PADL 2024, London, UK, January 15-16, 2024, Proceedings / / Martin Gebser and Ilya Sergey, editors |
Edizione | [First edition.] |
Pubbl/distr/stampa | Cham, Switzerland : , : Springer, , [2023] |
Descrizione fisica | 1 online resource (238 pages) |
Disciplina | 005.131 |
Collana | Lecture Notes in Computer Science Series |
Soggetto topico |
Declarative programming
Declarative programming languages |
ISBN | 3-031-52038-6 |
Formato | Materiale a stampa |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | Invited Talks -- Whats and Whys of Neural Network Verification (A Declarative Programming Perspective) -- Modular Higher-Order Effects -- Regular Papers -- Forget and Regeneration Techniques for Optimizing ASP-based Stream Reasoning -- Asynchronous Reactive Programming with Modal Types in Haskell -- FOLD-SE: An Efficient Rule-based Machine Learning Algorithm with Scalable Explainability -- Marketplace Logistics via Answer Set Programming -- Rhyme: A Data-Centric Expressive Query Language for Nested Data Structures -- Rethinking Answer Set Programming Templates -- Cutting the Cake Into Crumbs: Verifying Envy-Free Cake-Cutting Protocols using Bounded Integer Arithmetic -- A direct ASP Encoding for Declare -- Using Logic Programming and Kernel-Grouping for Improving Interpretability of Convolutional Neural Networks -- Hardware implementation of OCaml using a synchronous functional language -- Ontological Reasoning over Shy and Warded Datalog+/- for Streaming-based Architectures -- Explanation and Knowledge Acquisition in Ad Hoc Teamwork -- Automated Interactive Domain-Specific Conversational Agents that Understand Human Dialogs. |
Record Nr. | UNISA-996579166903316 |
Cham, Switzerland : , : Springer, , [2023] | ||
Materiale a stampa | ||
Lo trovi qui: Univ. di Salerno | ||
|
Programming languages and systems : 31st European Symposium on Programming, ESOP 2022, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2-7, 2022, Proceedings / / editor, Ilya Sergey |
Autore | Sergey Ilya |
Pubbl/distr/stampa | Cham, : Springer International Publishing AG, 2022 |
Descrizione fisica | 1 online resource (xiv, 604 pages) : illustrations |
Altri autori (Persone) | SergeyIlya |
Collana | Lecture notes in computer science |
Soggetto topico |
Computer programming
Programming languages (Electronic computers) |
Soggetto non controllato |
automata theory
computer programming computer systems databases distributed computer systems distributed systems embedded systems formal languages formal logic linguistics ontologies parallel processing systems program compilers programming languages semantics software design software engineering software quality verification |
ISBN | 3-030-99336-1 |
Formato | Materiale a stampa |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Record Nr. | UNINA-9910555236003321 |
Sergey Ilya | ||
Cham, : Springer International Publishing AG, 2022 | ||
Materiale a stampa | ||
Lo trovi qui: Univ. Federico II | ||
|
Programming languages and systems : 31st European Symposium on Programming, ESOP 2022, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2-7, 2022, Proceedings / / editor, Ilya Sergey |
Autore | Sergey Ilya |
Pubbl/distr/stampa | Cham, : Springer International Publishing AG, 2022 |
Descrizione fisica | 1 online resource (xiv, 604 pages) : illustrations |
Altri autori (Persone) | SergeyIlya |
Collana | Lecture notes in computer science |
Soggetto topico |
Computer programming
Programming languages (Electronic computers) |
Soggetto non controllato |
automata theory
computer programming computer systems databases distributed computer systems distributed systems embedded systems formal languages formal logic linguistics ontologies parallel processing systems program compilers programming languages semantics software design software engineering software quality verification |
ISBN | 3-030-99336-1 |
Formato | Materiale a stampa |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Record Nr. | UNISA-996464540903316 |
Sergey Ilya | ||
Cham, : Springer International Publishing AG, 2022 | ||
Materiale a stampa | ||
Lo trovi qui: Univ. di Salerno | ||
|
Programming languages and systems : 20th Asian symposium, APLAS 2022, Auckland, New Zealand, December 5, 2022, proceedings / / edited by Ilya Sergey |
Pubbl/distr/stampa | Cham, Switzerland : , : Springer, , [2022] |
Descrizione fisica | 1 online resource (222 pages) |
Disciplina | 005.13 |
Collana | Lecture Notes in Computer Science |
Soggetto topico | Programming languages (Electronic computers) |
ISBN |
9783031210372
9783031210365 |
Formato | Materiale a stampa |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto |
Intro -- Preface -- Organization -- Verification of Concurrent Programs Under Release Acquire (Invited Talk) -- Contents -- Semantics and Analysis -- An Algebraic Theory for Shared-State Concurrency -- 1 Introduction -- 2 Overview -- 2.1 Global-State (for Sequential Computation) -- 2.2 Shared-State -- 2.3 Denotations -- 2.4 Program Transformations -- 2.5 Caveats and Limitations -- 3 Equational Theory -- 4 A Monad for Shared-State -- 4.1 Difficulty of Term Normalization -- 4.2 Traces -- 4.3 Model Definition -- 4.4 Correspondence to Non-deterministic Global-State -- 4.5 Representation Theorem -- 4.6 Synchronization -- 5 Denotational Semantics -- 6 Metatheoretical Results -- 6.1 Example Transformations -- 7 Conclusion, Related Work, and Future Work -- References -- Decoupling the Ascending and Descending Phases in Abstract Interpretation -- 1 Introduction -- 2 Background -- 3 Decoupling the Ascending and Descending Phases -- 4 Experimental Evaluation -- 4.1 A Detailed Example -- 5 Related Work -- 6 Conclusion -- References -- Inferring Region Types via an Abstract Notion of Environment Transformation -- 1 Introduction -- 2 Background -- 2.1 Featherweight Java -- 2.2 Access Graphs -- 3 A Theory of Abstract Transformations -- 3.1 Types and Environments -- 3.2 Abstract Transformations -- 3.3 Operations on Abstract Transformations -- 4 Type Inference via Abstract Transformations -- 4.1 Region Type System -- 4.2 Inferring Region Types via Abstract Transformations -- 5 Conclusion, Implementation and Discussion -- References -- Testing and Verification -- RHLE: Modular Deductive Verification of Relational Properties -- 1 Introduction -- 2 The FunIMP Language -- 3 Approximating FunIMP Behaviors -- 3.1 Universal Executions -- 3.2 Existential Executions -- 3.3 Approximating Behaviors -- 4 RHLE -- 4.1 Synchronous Rules -- 4.2 Soundness -- 5 Verification.
6 Implementation and Evaluation -- 7 Related Work -- 8 Conclusion -- References -- Automated Temporal Verification for Algebraic Effects -- 1 Introduction -- 2 Overview -- 2.1 A Sense of ContEffs in File I/O -- 2.2 Effects Inferences via a Fixpoint Calculation -- 2.3 The TRS: To Prove Effects Inclusions -- 3 Language and Specifications -- 3.1 The Target Language -- 3.2 The Specification Language -- 3.3 Instrumented Semantics -- 4 Forward Verification -- 4.1 Forward Verification Rules -- 4.2 Fixpoint Computation -- 4.3 Reasoning in the Handling Program -- 5 Temporal Verification via a TRS -- 5.1 Rewriting Rules -- 6 Implementation and Evaluation -- 6.1 Case Studies -- 7 Related Work -- 8 Conclusion -- References -- Model-Based Fault Classification for Automotive Software -- 1 Introduction -- 2 Formal Model -- 3 Fault Localization -- 4 Fault Explanation -- 5 Fault Classification -- 6 Hoare Proofs with Timing -- 7 Application in Automotive Software -- 8 Related Work -- References -- Types -- Characterizing Functions Mappable over GADTs -- 1 Introduction -- 2 The Problem and Its Solution: An Overview -- 3 The Algorithm -- 4 Examples -- 5 Conclusion, Related Work, and Future Directions -- References -- Applicative Intersection Types -- 1 Introduction -- 2 Overview -- 2.1 Background -- 2.2 Applications of the Merge Operator -- 2.3 Challenges in the Design of the Semantics -- 2.4 Key Ideas and Results -- 3 Applicative Subtyping -- 3.1 Types and Subtyping -- 3.2 Applicative Subtyping -- 3.3 Metatheory -- 4 A Calculus with an Unrestricted Merge Operator -- 4.1 Syntax -- 4.2 Typing -- 4.3 Semantics -- 4.4 Type Soundness -- 5 A Calculus with a Disjoint Merge Operator -- 5.1 Disjointness -- 5.2 Typing and Semantics -- 5.3 Type Soundness and Determinism -- 6 Related Work -- 7 Conclusion and Future Work -- References. A Calculus with Recursive Types, Record Concatenation and Subtyping -- 1 Introduction -- 2 Overview -- 2.1 Background: Disjoint Intersection Types -- 2.2 i: Adding Recursive Types to i -- 2.3 Disjointness for Recursive Types -- 3 Static Semantics of i -- 3.1 Syntax and Subtyping -- 3.2 Decidability -- 3.3 Disjointness -- 3.4 Completeness of Disjointness -- 3.5 Bidirectional Typing -- 4 Dynamic Semantics of i -- 4.1 A Type-Directed Operational Semantics for i -- 4.2 Reduction -- 4.3 Determinism -- 4.4 Type Safety -- 5 Discussion and Related Work -- 6 Conclusion -- References -- Novice Type Error Diagnosis with Natural Language Models -- 1 Introduction -- 2 Approach -- 2.1 Language Models -- 2.2 The Pre-training and Fine-Tuning Scheme -- 2.3 Type Error Diagnosis as Token Classification -- 2.4 Structural Probe -- 3 Dataset and Evaluation Metric -- 3.1 Pre-training Dataset -- 3.2 Fine-Tuning Dataset -- 3.3 Evaluation Metric -- 4 Evaluation -- 4.1 Performance of Different Models (RQ1) -- 4.2 Effectiveness of Model Sizes and Transfer Learning (RQ2) -- 4.3 Generalization Ability of Language Models (RQ3) -- 4.4 Explaining Performance Difference by the Structural Probe (RQ4) -- 5 Related Work -- 6 Conclusions and Future Work -- References -- Author Index. |
Record Nr. | UNISA-996500061703316 |
Cham, Switzerland : , : Springer, , [2022] | ||
Materiale a stampa | ||
Lo trovi qui: Univ. di Salerno | ||
|
Programming languages and systems : 20th Asian symposium, APLAS 2022, Auckland, New Zealand, December 5, 2022, proceedings / / edited by Ilya Sergey |
Pubbl/distr/stampa | Cham, Switzerland : , : Springer, , [2022] |
Descrizione fisica | 1 online resource (222 pages) |
Disciplina | 005.13 |
Collana | Lecture Notes in Computer Science |
Soggetto topico | Programming languages (Electronic computers) |
ISBN |
9783031210372
9783031210365 |
Formato | Materiale a stampa |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto |
Intro -- Preface -- Organization -- Verification of Concurrent Programs Under Release Acquire (Invited Talk) -- Contents -- Semantics and Analysis -- An Algebraic Theory for Shared-State Concurrency -- 1 Introduction -- 2 Overview -- 2.1 Global-State (for Sequential Computation) -- 2.2 Shared-State -- 2.3 Denotations -- 2.4 Program Transformations -- 2.5 Caveats and Limitations -- 3 Equational Theory -- 4 A Monad for Shared-State -- 4.1 Difficulty of Term Normalization -- 4.2 Traces -- 4.3 Model Definition -- 4.4 Correspondence to Non-deterministic Global-State -- 4.5 Representation Theorem -- 4.6 Synchronization -- 5 Denotational Semantics -- 6 Metatheoretical Results -- 6.1 Example Transformations -- 7 Conclusion, Related Work, and Future Work -- References -- Decoupling the Ascending and Descending Phases in Abstract Interpretation -- 1 Introduction -- 2 Background -- 3 Decoupling the Ascending and Descending Phases -- 4 Experimental Evaluation -- 4.1 A Detailed Example -- 5 Related Work -- 6 Conclusion -- References -- Inferring Region Types via an Abstract Notion of Environment Transformation -- 1 Introduction -- 2 Background -- 2.1 Featherweight Java -- 2.2 Access Graphs -- 3 A Theory of Abstract Transformations -- 3.1 Types and Environments -- 3.2 Abstract Transformations -- 3.3 Operations on Abstract Transformations -- 4 Type Inference via Abstract Transformations -- 4.1 Region Type System -- 4.2 Inferring Region Types via Abstract Transformations -- 5 Conclusion, Implementation and Discussion -- References -- Testing and Verification -- RHLE: Modular Deductive Verification of Relational Properties -- 1 Introduction -- 2 The FunIMP Language -- 3 Approximating FunIMP Behaviors -- 3.1 Universal Executions -- 3.2 Existential Executions -- 3.3 Approximating Behaviors -- 4 RHLE -- 4.1 Synchronous Rules -- 4.2 Soundness -- 5 Verification.
6 Implementation and Evaluation -- 7 Related Work -- 8 Conclusion -- References -- Automated Temporal Verification for Algebraic Effects -- 1 Introduction -- 2 Overview -- 2.1 A Sense of ContEffs in File I/O -- 2.2 Effects Inferences via a Fixpoint Calculation -- 2.3 The TRS: To Prove Effects Inclusions -- 3 Language and Specifications -- 3.1 The Target Language -- 3.2 The Specification Language -- 3.3 Instrumented Semantics -- 4 Forward Verification -- 4.1 Forward Verification Rules -- 4.2 Fixpoint Computation -- 4.3 Reasoning in the Handling Program -- 5 Temporal Verification via a TRS -- 5.1 Rewriting Rules -- 6 Implementation and Evaluation -- 6.1 Case Studies -- 7 Related Work -- 8 Conclusion -- References -- Model-Based Fault Classification for Automotive Software -- 1 Introduction -- 2 Formal Model -- 3 Fault Localization -- 4 Fault Explanation -- 5 Fault Classification -- 6 Hoare Proofs with Timing -- 7 Application in Automotive Software -- 8 Related Work -- References -- Types -- Characterizing Functions Mappable over GADTs -- 1 Introduction -- 2 The Problem and Its Solution: An Overview -- 3 The Algorithm -- 4 Examples -- 5 Conclusion, Related Work, and Future Directions -- References -- Applicative Intersection Types -- 1 Introduction -- 2 Overview -- 2.1 Background -- 2.2 Applications of the Merge Operator -- 2.3 Challenges in the Design of the Semantics -- 2.4 Key Ideas and Results -- 3 Applicative Subtyping -- 3.1 Types and Subtyping -- 3.2 Applicative Subtyping -- 3.3 Metatheory -- 4 A Calculus with an Unrestricted Merge Operator -- 4.1 Syntax -- 4.2 Typing -- 4.3 Semantics -- 4.4 Type Soundness -- 5 A Calculus with a Disjoint Merge Operator -- 5.1 Disjointness -- 5.2 Typing and Semantics -- 5.3 Type Soundness and Determinism -- 6 Related Work -- 7 Conclusion and Future Work -- References. A Calculus with Recursive Types, Record Concatenation and Subtyping -- 1 Introduction -- 2 Overview -- 2.1 Background: Disjoint Intersection Types -- 2.2 i: Adding Recursive Types to i -- 2.3 Disjointness for Recursive Types -- 3 Static Semantics of i -- 3.1 Syntax and Subtyping -- 3.2 Decidability -- 3.3 Disjointness -- 3.4 Completeness of Disjointness -- 3.5 Bidirectional Typing -- 4 Dynamic Semantics of i -- 4.1 A Type-Directed Operational Semantics for i -- 4.2 Reduction -- 4.3 Determinism -- 4.4 Type Safety -- 5 Discussion and Related Work -- 6 Conclusion -- References -- Novice Type Error Diagnosis with Natural Language Models -- 1 Introduction -- 2 Approach -- 2.1 Language Models -- 2.2 The Pre-training and Fine-Tuning Scheme -- 2.3 Type Error Diagnosis as Token Classification -- 2.4 Structural Probe -- 3 Dataset and Evaluation Metric -- 3.1 Pre-training Dataset -- 3.2 Fine-Tuning Dataset -- 3.3 Evaluation Metric -- 4 Evaluation -- 4.1 Performance of Different Models (RQ1) -- 4.2 Effectiveness of Model Sizes and Transfer Learning (RQ2) -- 4.3 Generalization Ability of Language Models (RQ3) -- 4.4 Explaining Performance Difference by the Structural Probe (RQ4) -- 5 Related Work -- 6 Conclusions and Future Work -- References -- Author Index. |
Record Nr. | UNINA-9910632482203321 |
Cham, Switzerland : , : Springer, , [2022] | ||
Materiale a stampa | ||
Lo trovi qui: Univ. Federico II | ||
|