- arXiv.org
- Popular Physics
- Space Physics
- History and Philosophy of Physics
- Optics
- Atomic and Molecular Clusters
- Physics and Society
- Data Analysis, Statistics and Probability
- Fluid Dynamics
- Biological Physics
- General Physics
- Geophysics
- Atomic Physics
- Plasma Physics
- Medical Physics
- Physics Education
- Instrumentation and Detectors
- Classical Physics
- Chemical Physics
- Computational Physics
- Accelerator Physics
- Atmospheric and Oceanic Physics

- Number Theory
- Analysis of PDEs
- Information Theory
- Statistics Theory
- History and Overview
- Mathematical Physics
- Combinatorics
- Operator Algebras
- Algebraic Geometry
- Probability
- Representation Theory
- Complex Variables
- Symplectic Geometry
- Group Theory
- Quantum Algebra
- Optimization and Control
- General Topology
- Dynamical Systems
- Geometric Topology
- Numerical Analysis
- Differential Geometry
- Metric Geometry
- Logic
- General Mathematics
- Spectral Theory
- Category Theory
- Rings and Algebras
- Algebraic Topology
- Classical Analysis and ODEs
- K-Theory and Homology
- Commutative Algebra
- Functional Analysis

- Information Retrieval
- Information Theory
- General Literature
- Formal Languages and Automata Theory
- Computational Engineering, Finance, and Science
- Symbolic Computation
- Emerging Technologies
- Learning
- Computer Vision and Pattern Recognition
- Neural and Evolutionary Computing
- Programming Languages
- Social and Information Networks
- Multiagent Systems
- Databases
- Sound
- Software Engineering
- Operating Systems
- Computer Science and Game Theory
- Hardware Architecture
- Artificial Intelligence
- Systems and Control
- Distributed, Parallel, and Cluster Computing
- Cryptography and Security
- Discrete Mathematics
- Digital Libraries
- Human-Computer Interaction
- Numerical Analysis
- Performance
- Mathematical Software
- Computational Complexity
- Other Computer Science
- Computation and Language
- Logic in Computer Science
- Robotics
- Data Structures and Algorithms
- Computational Geometry
- Computers and Society
- Networking and Internet Architecture
- Multimedia
- Graphics

- Following previous work on CCS, we propose a compositional model for the $\pi$-calculus in which processes are interpreted as sheaves on certain simple sites. Such sheaves are a concurrent form of innocent strategies, in the sense of Hyland-Ong/Nickau game semantics. We define an analogue of fair testing equivalence in the model and show that our interpretation is intensionally fully abstract for it. That is, the interpretation preserves and reflects fair testing equivalence; and furthermore, any innocent strategy is fair testing equivalent to the interpretation of some process. The central part of our work is the construction of our sites, relying on a combinatorial presentation of $\pi$-calculus traces in the spirit of string diagrams.
- This paper presents an approach to lemma synthesis to support advanced inductive entailment procedures based on separation logic. We first propose a mechanism where lemmas are automatically proven and systematically applied. The lemmas may include universal guard and/or unknown predicate. While the former is critical for expressivity, the latter is essential for supporting relationships between multiple predicates. We further introduce lemma synthesis to support (i) automated inductive reasoning together with frame inference and (ii) theorem exploration. For (i) we automatically discover and prove auxiliary lemmas during an inductive proof; and for (ii) we automatically generate a useful set of lemmas to relate user-defined or system-generated predicates. We have implemented our proposed approach into an existing verification system and tested its capability in inductive reasoning and theorem exploration. The experimental results show that the enhanced system can automatically synthesize useful lemmas to facilitate reasoning on a broad range of non-trivial inductive proofs.
- Chain reduction enables reduced ordered binary decision diagrams (BDDs) and zero-suppressed binary decision diagrams (ZDDs) to each take advantage of the others' ability to symbolically represent Boolean functions in compact form. For any Boolean function, its chain-reduced ZDD (CZDD) representation will be no larger than its ZDD representation, and at most twice the size of its BDD representation. The chain-reduced BDD (CBDD) of a function will be no larger than its BDD representation, and at most three times the size of its CZDD representation. Extensions to the standard algorithms for operating on BDDs and ZDDs enable them to operate on the chain-reduced versions. Experimental evaluations on representative benchmarks for encoding word lists, solving combinatorial problems, and operating on digital circuits indicate that chain reduction can provide significant benefits in terms of both memory and execution time.
- In this paper we propose a formal framework for studying privacy in information systems. The proposal follows a two-axes schema where the first axis considers privacy as a taxonomy of rights and the second axis involves the ways an information system stores and manipulates information. We develop a correspondence between the above schema and an associated model of computation. In particular, we propose the \Pcalc, a calculus based on the $\pi$-calculus with groups extended with constructs for reasoning about private data. The privacy requirements of an information system are captured via a privacy policy language. The correspondence between the privacy model and the \Pcalc semantics is established using a type system for the calculus and a satisfiability definition between types and privacy policies. We deploy a type preservation theorem to show that a system respects a policy and it is safe if the typing of the system satisfies the policy. We illustrate our methodology via analysis of two use cases: a privacy-aware scheme for electronic traffic pricing and a privacy-preserving technique for speed-limit enforcement.

A Rational Agent Controlling an Autonomous Vehicle: Implementation and Fo...

Martin Henessey Oct 03 2017 01:48 UTCZoltán Zimborás May 28 2014 04:42 UTC

It's a bit funny to look at a formally verified proof of the CLT :), here it is online:

https://github.com/avigad/isabelle.