the proceedings contain 30 papers. the special focus in this conference is on programminglanguages and systems. the topics include: Simple and precise widenings for H-polyhedra;metric spaces and termination analyses;...
ISBN:
(纸本)9783642171635
the proceedings contain 30 papers. the special focus in this conference is on programminglanguages and systems. the topics include: Simple and precise widenings for H-polyhedra;metric spaces and termination analyses;amortized resource analysis with polymorphic recursion and partial big-step operational semantics;interprocedural control flow reconstruction;data structure fusion;categorical descriptional composition;bisimulation proof methods in a path-based specification language for polynomial coalgebras;Context-preserving XQuery fusion;index-compact garbage collection;foundations of quantum programming;live heap space bounds for real-time systems;a quick tour of the verifast program verifier;verification of tree-processing programs via higher-order model checking;automatically inferring quantified loop invariants by algorithmic learning from simple templates;relational parametricity for a polymorphic linear lambda calculus;A certified implementation of ML with structural polymorphism;type inference for sublinear space functional programming;liveness of communicating transactions;model independent order relations for processes;concurrency can’t be observed, asynchronously;from a verified kernel towards verified systems;a logical mix of approximation and separation;reasoning about computations using two-levels of logic;typechecking higher-order security libraries;towards deriving type systems and implementations for coroutines;liberal typing for functional logic programs;a provably correct stackless intermediate representation for Java bytecode;JNI light: An operational model for the core JNI.
the proceedings contain 30 papers. the topics discussed include: foundations of quantum programming;from a verified kernel towards verified systems;reasoning about computations using two-levels of logic;towards derivi...
ISBN:
(纸本)364217163X
the proceedings contain 30 papers. the topics discussed include: foundations of quantum programming;from a verified kernel towards verified systems;reasoning about computations using two-levels of logic;towards deriving type systems and implementations for coroutines;liberal typing for functional logic programs;a provably correct stackless intermediate representation for java bytecode;metric spaces and termination analyses;amortized resource analysis with polymorphic recursion and partial big-step operational semantics;interprocedural control flow reconstruction;data structure fusion;bisimulation proof methods in a path-based specification language for polynomial coalgebras;index-compact garbage collection;live heap space bounds for real-time systems;a quick tour of the verifast program verifier;and verification of tree-processing programs via higher-order model checking.
the proceedings contain 23 papers. the topics discussed include: modeling of problem domains for driving program development systems;programming primitives for database languages;paths: an abstract alternative to poin...
ISBN:
(纸本)089791029X
the proceedings contain 23 papers. the topics discussed include: modeling of problem domains for driving program development systems;programming primitives for database languages;paths: an abstract alternative to pointers;program improvement by internal specialization;paging as a 'language processing' task;position paper on optimizing compilers;making the world safe for garbage collection;carrier arrays: an idiom-preserving extension to APL;axiomatic definitions of programminglanguages, II;formal program testing;the temporal logic of branching time;program logic without binding is decidable;on the advantages of free choice: a symmetric and fully distributed solution to the dining philosophers problem;a program development tool;program verification based on denotational semantics;incremental evaluation for attribute grammars with application to syntax-directed editors;linear cost is sometimes quadratic;a precise inter-procedural data flow algorithm;verification of attribute grammar;dependence graphs and compiler optimizations;program optimization and exception handling;and inferring types in Smalltalk.
the proceedings contain 22 papers. the special focus in this conference is on programminglanguages and systems. the topics include: New Approaches for Almost-Sure Termination of Probabilistic Programs;particle-Style ...
ISBN:
(纸本)9783030027674
the proceedings contain 22 papers. the special focus in this conference is on programminglanguages and systems. the topics include: New Approaches for Almost-Sure Termination of Probabilistic Programs;particle-Style Geometry of Interaction as a Module System;automated Synthesis of Functional Programs with Auxiliary Functions;Modular Verification of SPARCv8 Code;formal Small-Step Verification of a Call-by-Value Lambda Calculus Machine;automated Modular Verification for Relaxed Communication Protocols;automated Proof Synthesis for the Minimal Propositional Logic with Deep Neural Networks;on the Complexity of Pointer Arithmetic in Separation Logic;a Decision Procedure for String Logic with Quadratic Equations, Regular Expressions and Length Constraints;factoring Derivation Spaces via Intersection Types;Certifying CPS Transformation of Let-Polymorphic Calculus Using PHOAS;model Checking Differentially Private Properties;shallow Effect Handlers;types of Fireballs;on the Soundness of Call Graph Construction in the Presence of Dynamic Language Features - A Benchmark and Tool Evaluation;complexity Analysis of Tree Share Structure;relational thread-Modular Abstract Interpretation Under Relaxed Memory Models;scallina: Translating Verified Programs from Coq to Scala;HoIce: An ICE-Based Non-linear Horn Clause Solver;traf: A Graphical Proof Tree Viewer Cooperating with Coq through Proof General.
the proceedings contain 36 papers. the special focus in this conference is on Typing and Structuring systems. the topics include: Calculate polytypically;limits of ML-definability;functorial ML;parametric polymorphism...
ISBN:
(纸本)3540617566
the proceedings contain 36 papers. the special focus in this conference is on Typing and Structuring systems. the topics include: Calculate polytypically;limits of ML-definability;functorial ML;parametric polymorphism for typed prolog and a-prolog;a specification formalism for inheritance and object hierarchies;towards independent and-parallelism in CLP;annotated structure shape graphs for abstract analysis of prolog;a reactive implementation of pos using ROBDDs;dynamic attribute grammars;controlling conjunctive partial deduction;unfold/fold transformations of concurrent processes;semantics-based compiling;implementing memoization for partial evaluation;higher order deforestation;scheduling expression DAGs for minimal register need;improving tabled logic programs through alternative scheduling strategies;a new implementation approach for prolog;systematic extraction and implementation of divide-and-conquer parallelism;functional skeletons generate process topologies in eden;a language for executable specifications;from term rewriting to generalised interaction nets;type isomorphisms for module signatures;decidability of logic program semantics and applications to testing;unifying pictures and widgets in a constraint-based framework for concurrent functional GUI;modeling sharing and recursion for weak reduction strategies using explicit substitution;context-sensitive computations in confluent programs;models for using stochastic constraint solvers in constraint logic programming;integrating efficient records into concurrent constraint programming;the LOL deductive database programming language;an efficient and precise sharing domain for logic programs;cheap tupling in calculational form;needed narrowing in prolog;automatic optimization of dynamic scheduling in logic programs and a visual constraint programming tool.
the *** project has produced a formal, machine-checked Isabelle/HOL proof that the C code of the seL4 OS microkernel correctly implements its abstract implementation. this paper briefly summarises the proof, its main ...
详细信息
ISBN:
(纸本)9783642171635
the *** project has produced a formal, machine-checked Isabelle/HOL proof that the C code of the seL4 OS microkernel correctly implements its abstract implementation. this paper briefly summarises the proof, its main implications and assumptions, reports on the experience in conducting such a large-scale verification, and finally lays out a vision how this formally verified kernel may be used for gaining formal, code-level assurance about safety and security properties of systems on the order of a million lines of code.
We consider programming language aspects of algorithms that operate on data too large to fit into memory. In previous work we have introduced intML, a functional programming language with primitives that support the i...
详细信息
ISBN:
(纸本)9783642171635
We consider programming language aspects of algorithms that operate on data too large to fit into memory. In previous work we have introduced intML, a functional programming language with primitives that support the implementation of such algorithms. We have shown that IntML can express all LOGS PACE functions but have left open the question how easy it is in practice to program typical LOGSPACE algorithms in IntML. In this paper we develop algorithms for intmL type inference. We show that with type inference one can handle programs that could not be reasonably manipulated by hand. We do so by implementing in IntML, a typical LOGSPACE algorithm, a test for acyclicity of undirected graphs. thus we show that with type inference Irian can express typical algorithmic patterns of LOGSPACE easily and in a natural way.
Bisimulation is one of the fundamental concepts of the theory of coalgebras. However, it is difficult to verify whether a relation is a bisimulation. Although some categorical bisimulation proof methods for coalgebras...
详细信息
ISBN:
(纸本)9783642171635
Bisimulation is one of the fundamental concepts of the theory of coalgebras. However, it is difficult to verify whether a relation is a bisimulation. Although some categorical bisimulation proof methods for coalgebras have been proposed, they are not based on specification languages of coalgebras so that they are difficult to be used in practice. In this paper, a specification language based on paths of polynomial functors is proposed to specify polynomial coalgebras. Since bisimulation can be defined by paths, it is easy to transform Sangiorgi's bisimulation proof methods for labeled transition systems to reasoning rules in such a path-based specification language for polynomial coalgebras. the paper defines the notions of progressions and sound functions based on paths, then introduces the notion of faithful contexts for the language and presents a bisimulation-up-to context proof technique for polynomial coalgebras. Several examples are given to illustrate how to make use of the bisimulation proof methods in the language.
this paper describes the main features of VeriFast, a sound and modular program verifier for C and Java. VeriFast takes as input a number of source files annotated with method contracts written in separation logic, in...
详细信息
ISBN:
(纸本)9783642171635
this paper describes the main features of VeriFast, a sound and modular program verifier for C and Java. VeriFast takes as input a number of source files annotated with method contracts written in separation logic, inductive data type and fixpoint definitions, lemma functions and proof steps. the verifier checks that (1) the program does not perform illegal operations such as dividing by zero or illegal memory accesses and (2) that the assumptions described in method contracts hold in each execution. Although VeriFast supports specifying and verifying deep data structure properties, it provides an interactive verification experience as verification times are consistently low and errors can be diagnosed using its symbolic debugger. VeriFast and a large number of example programs are available online at: http : / /www. cs . kuleuven. be/similar to bartj/verifast
Progress in the techniques of quantum devices has made people widely believe that large-scale and functional quantum computers will be eventually built. By then, super-powered quantum computer will solve many problems...
详细信息
暂无评论