The proceedings contain 15 papers. The topics discussed include: the machinery of interaction;a computational understanding of classical (co)recursion;degrading lists;verified linear session-typed concurrent programmi...
ISBN:
(纸本)9781450388214
The proceedings contain 15 papers. The topics discussed include: the machinery of interaction;a computational understanding of classical (co)recursion;degrading lists;verified linear session-typed concurrent programming;inversion framework: reasoning about inversion by conditional term rewriting systems;finding candidate keys and 3NF via strategic port graph rewriting;rewrites as terms through justification logic;hailstorm : a statically-typed, purely functional language for IoT applications;understanding Lua’s garbage collection: towards a formalized static analyzer;and Moulinog: a generator of random student assignments written in prolog.
The proceedings contain 14 papers. The special focus in this conference is on Practical Aspects of Declarative languages. The topics include: Whitebox Induction of Default Rules Using High-Utility Itemset Mining;expla...
ISBN:
(纸本)9783030391966
The proceedings contain 14 papers. The special focus in this conference is on Practical Aspects of Declarative languages. The topics include: Whitebox Induction of Default Rules Using High-Utility Itemset Mining;explanations for Dynamic programming;A DSL for Integer Range Reasoning: Partition, Interval and Mapping Diagrams;variability-Aware Datalog;flexible Graph Matching and Graph Edit Distance Using Answer Set programming;on Repairing Web Services Workflows;AQuA: ASP-Based Visual Question Answering;diagnosing Data Pipeline Failures Using Action languages: A Progress Report;VRASP: A Virtual Reality Environment for Learning Answer Set programming;On the Effects of Integrating Region-Based Memory Management and Generational Garbage Collection in ML;RTMLton: An SML Runtime for Real-Time systems;A Timed IO Monad.
There is a growing interest in leveraging functional programminglanguages in real-time and embedded contexts. Functional languages are appealing as many are strictly typed, amenable to formal methods, have limited mu...
详细信息
ISBN:
(纸本)9783030391973;9783030391966
There is a growing interest in leveraging functional programminglanguages in real-time and embedded contexts. Functional languages are appealing as many are strictly typed, amenable to formal methods, have limited mutation, and have simple, but powerful con-currency control mechanisms. Although there have been many recent proposals for specialized domain specific languages for embedded and real-time systems, there has been relatively little progress on adapting more general purpose functional languages for programming embedded and real-time systems. In this paper we present our current work on leveraging Standard ML in the embedded and real-time domains. Specifically we detail our experiences in modifying MLton, a whole program, optimizing compiler for Standard ML, for use in such contexts. We focus primarily on the language runtime, re-working the threading subsystem and garbage collector. We provide preliminary results over a radar-based aircraft collision detector ported to SML.
Answer Set programming (ASP) is a dominant programming paradigm in Knowledge Representation. It is used to build intelligent agents - knowledge-intensive software systems capable of exhibiting intelligent behaviors. I...
详细信息
ISBN:
(纸本)9783030391973;9783030391966
Answer Set programming (ASP) is a dominant programming paradigm in Knowledge Representation. It is used to build intelligent agents - knowledge-intensive software systems capable of exhibiting intelligent behaviors. It is found that ASP can also be used to teach computer science in middle and high schools. However, the current ASP systems do not provide direct support for a programmer to produce an intelligent agent that a general user can directly interact with, which may greatly compromise the potential attraction of ASP to the secondary school students. In this paper, we propose a Virtual Reality (VR) programming environment called VRASP that allows a student to produce an avatar (agent) in a virtual world that is able to answer questions in spoken natural language from a general user. The VR application is accessible from anywhere so that the students' friends can interact with the agent. As a result, it gives the students a feeling of achievement and thus encourages them to solve problems using ASP. VRASP was evaluated with 10 users. Results of these studies show that students are able to communicate with the environment intuitively with an accuracy of 78%.
Bounded treewidth is one of the most cited combinatorial invariants, which was applied in the literature for solving several counting problems efficiently. A canonical counting problem is #Sat, which asks to count the...
详细信息
ISBN:
(纸本)9783030391973;9783030391966
Bounded treewidth is one of the most cited combinatorial invariants, which was applied in the literature for solving several counting problems efficiently. A canonical counting problem is #Sat, which asks to count the satisfying assignments of a Boolean formula. Recent work shows that benchmarking instances for #Sat often have reasonably small treewidth. This paper deals with counting problems for instances of small treewidth. We introduce a general framework to solve counting questions based on state-of-the-art database management systems (DBMS). Our framework takes explicitly advantage of small treewidth by solving instances using dynamic programming (DP) on tree decompositions (TD). Therefore, we implement the concept of DP into a DBMS (PostgreSQL), since DP algorithms are already often given in terms of table manipulations in theory. This allows for elegant specifications of DP algorithms and the use of SQL to manipulate records and tables, which gives us a natural approach to bring DP algorithms into practice. To the best of our knowledge, we present the first approach to employ a DBMS for algorithms on TDs. A key advantage of our approach is that DBMS naturally allow to deal with huge tables with a limited amount of main memory (RAM), parallelization, as well as suspending computation.
While the object-orientation is the most used paradigm for developing general purpose software systems, the use of reactive systems has been growing lately. One of the differences between them is that while the first ...
详细信息
We explore a programming approach for concurrency that synchronizes all accesses to shared memory by default. Synchronization takes place by ensuring that all program code runs inside atomic sections even if the progr...
详细信息
ISBN:
(纸本)9781450344937
We explore a programming approach for concurrency that synchronizes all accesses to shared memory by default. Synchronization takes place by ensuring that all program code runs inside atomic sections even if the program code has external side effects. Threads are mapped to atomic sections that a programmer must explicitly split to increase concurrency. A naive implementation of this approach incurs a large amount of overhead. We show how to reduce this overhead to make the approach suitable for realistic application programs on existing hardware. We present an implementation technique based on a special-purpose software transactional memory system. To reduce the overhead, the technique exploits properties of managed, object-oriented programminglanguages as well as intraprocedural static analyses and uses field-level granularity locking in combination with transactional I/O to provide good scaling properties. We implemented the synchronized-by-default (SBD) approach for the Java language and evaluate its performance for six programs from the DaCapo benchmark suite. The evaluation shows that, compared to explicit synchronization, the SBD approach has an overhead between 0.4% and 102% depending on the benchmark and the number of threads, with a mean (geom.) of 23.9%.
The proceedings contain 18 papers. The special focus in this conference is on Static Analysis. The topics include: Static analysis of non-interference in expressive low-level languages;static analysis with set-closure...
ISBN:
(纸本)9783662482872
The proceedings contain 18 papers. The special focus in this conference is on Static Analysis. The topics include: Static analysis of non-interference in expressive low-level languages;static analysis with set-closure in secrecy;a binary decision tree abstract domain functor;precise data flow analysis in the presence of correlated method calls;may-happen-in-parallel analysis for asynchronous programs with inter-procedural synchronization;shape analysis for unstructured sharing;synthesizing heap manipulations via integer linear programming;effective soundness-guided reflection analysis;a type system for javascript with fixed object layout;refinement type inference via horn constraint optimization;a simple abstraction of arrays and maps by program translation;property-based polynomial invariant generation using sums-of-squares optimization;a case study on the correspondence between top-down and bottom-up analysis;parallel cost analysis of distributed systems;a forward analysis for recurrent sets and unbounded-time analysis of guarded LTI systems with inputs by abstract acceleration.
The proceedings contain 32 papers. The topics discussed include: the compiler forest;pretty-big-step semantics;language constructs for non-well-founded computation;laziness by need;compositional invariant checking for...
ISBN:
(纸本)9783642370359
The proceedings contain 32 papers. The topics discussed include: the compiler forest;pretty-big-step semantics;language constructs for non-well-founded computation;laziness by need;compositional invariant checking for overlaid and nested linked lists;a discipline for program verification based on backpointers and its use in observational disjointness;modular reasoning about separation of concurrent data structures;ribbon proofs for separation logic;abstract refinement types;constraining delimited control with contracts;verifying concurrent memory reclamation algorithms with grace;verifying concurrent programs against sequential specifications;behavioral polymorphism and parametricity in session-based communication;higher-order processes, functions, and sessions: a monadic integration;and structural lock correlation with ownership types.
While generalized algebraic datatypes (GADTs) are now considered well-understood, adding them to a language with a notion of subtyping comes with a few surprises. What does it mean for a GADT parameter to be covariant...
详细信息
ISBN:
(纸本)9783642370366
While generalized algebraic datatypes (GADTs) are now considered well-understood, adding them to a language with a notion of subtyping comes with a few surprises. What does it mean for a GADT parameter to be covariant? The answer turns out to be quite subtle. It involves fine-grained properties of the subtyping relation that raise interesting design questions. We allow variance annotations in GADT definitions, study their soundness, and present a sound and complete algorithm to check them. Our work may be applied to real-world ML-like languages with explicit subtyping such as OCaml, or to languages with general subtyping constraints.
暂无评论