The proceedings contain 18 papers. The special focus in this conference is on programminglanguages andsystems. The topics include: Random-Access Lists, from EE to FP;generic Reasoning of the Locally Namele...
ISBN:
(纸本)9789819789429
The proceedings contain 18 papers. The special focus in this conference is on programminglanguages andsystems. The topics include: Random-Access Lists, from EE to FP;generic Reasoning of the Locally Nameless Representation;building a Correct-by-Construction Type Checker for a Dependently Typed Core Language;extending the Quantitative Pattern-Matching Paradigm;hybrid Verification of Declarative Programs with Arithmetic Non-fail Conditions;explaining Explanations in Probabilistic Logic programming;quantum programming Without the Quantum Physics;quantum Bisimilarity Is a Congruence Under Physically Admissible Schedulers;non-deterministic, Probabilistic, and Quantum Effects Through the Lens of Event Structures;type-Based Verification of Connectivity Constraints in Lattice Surgery;on Computational Indistinguishability and Logical Relations;relative Completeness of Incorrectness Separation Logic;OBRA: Oracle-Based, Relational, Algorithmic Type Verification;a Formal Verification Framework for Tezos Smart Contracts Based on Symbolic Execution;mode-based Reduction from Validity Checking of Fixpoint Logic Formulas to Test-Friendly Reachability Problem;efficiently Adapting Stateless Model Checking for C11/C++11 to Mixed-Size Accesses.
Dependently typed languages allow us to state a program's expected properties and automatically check that they are satisfied at compile time. Yet the implementations of these languages are themselves just softwar...
详细信息
ISBN:
(纸本)9789819789429;9789819789436
Dependently typed languages allow us to state a program's expected properties and automatically check that they are satisfied at compile time. Yet the implementations of these languages are themselves just software, so can we really trust them? The goal of this paper is to develop a lightweight technique to improve their trustworthiness by giving a formal specification of the typing rules and intrinsically verifying the type checker with respect to these rules. Concretely, we apply this technique to a subset of Agda's internal language, implemented in Agda. Our development relies on erasure annotations to separate the specification from the runtime of the type checker. We provide guidelines for making design decisions for certified core type checkers and evaluate trade-offs.
Numerical representations, which were popularized by Okasaki in his seminal book [1], decouple the design of data-types into, first, a choice of a data-structure encoding a suitable numerical system, followed by decor...
详细信息
ISBN:
(纸本)9789819789429;9789819789436
Numerical representations, which were popularized by Okasaki in his seminal book [1], decouple the design of data-types into, first, a choice of a data-structure encoding a suitable numerical system, followed by decorating this structure with as many pieces of data as specified by the underlying numerical system. This paper ambitions to apply McBride's theory of ornaments [2] to explore a structural interpretation of numerical representation. In particular, we propose a journey from Electronic Engineering -computing with binary numbers-to Functional programming -implementing a persistent random-access list datatype.
Functions containing arithmetic operations have often restrictions not expressible by standard type systems of programminglanguages. The division operation requires that the divisor is non-zero and the factorial func...
详细信息
ISBN:
(纸本)9789819789429;9789819789436
Functions containing arithmetic operations have often restrictions not expressible by standard type systems of programminglanguages. The division operation requires that the divisor is non-zero and the factorial function should not be applied to negative numbers. Such partial operations might lead to program crashes if they are applied to unintended arguments. Checking the arguments before each call is tedious and decreases the run-time efficiency. To avoid these disadvantages and support the safe use of partially defined operations, we present an approach to verify the correct use of operations at compile time. To simplify its use, our approach automatically infers non-fail conditions of operations from their definitions and checks whether these conditions are satisfied for all uses of the operations. Arithmetic conditions can be verified by SMT solvers, whereas conditions in operations defined on algebraic data types can be inferred and verified by appropriate type abstractions. Therefore, we present a hybrid method which is applicable to larger programs since only a few arithmetic non-fail conditions need to be checked by an external SMT solver. This approach is implemented for functional logic Curry programs so that it is also usable for purely functional or logic programs.
We propose a quantum programming paradigm where all data are familiar classical data, and the only non-classical element is a random number generator that can return results with negative probability. Currently, the v...
详细信息
ISBN:
(纸本)9789819789429;9789819789436
We propose a quantum programming paradigm where all data are familiar classical data, and the only non-classical element is a random number generator that can return results with negative probability. Currently, the vast majority of quantum programminglanguages instead work with quantum data types made up of qubits. The description of their behavior relies on heavy linear algebra and many interdependent concepts and intuitions from quantum physics, which takes dedicated study to understand. We demonstrate that the proposed view of quantum programming explains its central concepts and constraints in more accessible, computationally relevant terms. This is achieved by systematically reducing everything to the existence of that negative-probability random generator, avoiding mention of advanced physics. This makes quantum programming more accessible to programmers without a deep background in physics or linear algebra. The bulk of this paper is written with such an audience in mind. As a working vehicle, we lay out a simple quantum programming language under this paradigm, showing that not only can it express all quantum algorithms, it also naturally captures the semantics of measurement without ever mentioning qubits or collapse.
We show how (well-established) type systems based on non-idempotent intersection types can be extended to characterize termination properties of functional programminglanguages with pattern matching features. To mode...
详细信息
ISBN:
(纸本)9789819789429;9789819789436
We show how (well-established) type systems based on non-idempotent intersection types can be extended to characterize termination properties of functional programminglanguages with pattern matching features. To model such programminglanguages, we use a (weak and closed) lambda-calculus integrating a pattern matching mechanism on algebraic data types (ADTs). Remarkably, we also show that this language not only encodes Plotkin's CBV and CBN lambda-calculus as well as other subsuming frameworks, such as the bang-calculus, but can also be used to interpret the semantics of effectful languages with exceptions. After a thorough study of the untyped language, we introduce a type system based on intersection types, and we show through purely logical methods that the set of terminating terms of the language corresponds exactly to that of well-typed terms. Moreover, by considering non-idempotent intersection types, this characterization turns out to be quantitative, i.e. the size of the type derivation of a term t gives an upper bound for the number of evaluation steps from t to its normal form.
The emergence of tools based on artificial intelligence has also led to the need of producing explanations which are understandable by a human being. In most approaches, the system is considered a black box, making it...
详细信息
ISBN:
(纸本)9789819789429;9789819789436
The emergence of tools based on artificial intelligence has also led to the need of producing explanations which are understandable by a human being. In most approaches, the system is considered a black box, making it difficult to generate appropriate explanations. In this work, though, we consider a setting where models are transparent: probabilistic logic programming (PLP), a paradigm that combines logic programming for knowledge representation and probability to model uncertainty. However, given a query, the usual notion of explanation is associated with a set of choices, one for each random variable of the model. Unfortunately, such a set does not explain why the query is true and, in fact, it may contain choices that are actually irrelevant for the considered query. To improve this situation, we present in this paper an approach to explaining explanations which is based on defining a new query-driven inference mechanism for PLP where proofs are labeled with choice expressions, a compact and easy to manipulate representation for sets of choices. The combination of proof trees and choice expressions allows us to produce comprehensible query justifications with a causal structure.
The proceedings contain 7 papers. The topics discussed include: checking process-oriented operating system behavior using CSP and refinement;a microkernel API for fine-grained decomposition;code-partitioning gossip;ca...
ISBN:
(纸本)9781605588445
The proceedings contain 7 papers. The topics discussed include: checking process-oriented operating system behavior using CSP and refinement;a microkernel API for fine-grained decomposition;code-partitioning gossip;catchandretry: extending exceptions to handle distributed system failures and recovery;filet-o-fish: practical and dependable domain-specific languages for OS development;Kstruct: preserving consistency through c annotations;and distributed data flow language for multi-party protocols.
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.
暂无评论