We gratefully acknowledge support from
the Simons Foundation and member institutions.

Logic in Computer Science

New submissions

[ total of 11 entries: 1-11 ]
[ showing up to 2000 entries per page: fewer | more ]

New submissions for Mon, 2 Aug 21

[1]  arXiv:2107.14283 [pdf, ps, other]
Title: Syllepsis in Homotopy Type Theory
Subjects: Logic in Computer Science (cs.LO)

It is well-known that in homotopy type theory (HoTT), one can prove the Eckmann-Hilton theorem: given two 2-loops p, q : 1 = 1 on the reflexivity path at an arbitrary point a : A, we have pq = qp. If we go one dimension higher, i.e., if p and q are 3-loops, we show that a property classically known as syllepsis also holds in HoTT: namely, the Eckmann-Hilton proof for q and p is the inverse of the Eckmann-Hilton proof for p and q.

[2]  arXiv:2107.14487 [pdf, other]
Title: Refining Labelled Systems for Modal and Constructive Logics with Applications
Authors: Tim Lyon
Comments: PhD Thesis
Subjects: Logic in Computer Science (cs.LO); Artificial Intelligence (cs.AI); Discrete Mathematics (cs.DM); Formal Languages and Automata Theory (cs.FL); Logic (math.LO)

This thesis introduces the "method of structural refinement", which serves as a means of transforming the relational semantics of a modal and/or constructive logic into an 'economical' proof system by connecting two proof-theoretic paradigms: labelled and nested sequent calculi. The formalism of labelled sequents has been successful in that cut-free calculi in possession of desirable proof-theoretic properties can be automatically generated for large classes of logics. Despite these qualities, labelled systems make use of a complicated syntax that explicitly incorporates the semantics of the associated logic, and such systems typically violate the subformula property to a high degree. By contrast, nested sequent calculi employ a simpler syntax and adhere to a strict reading of the subformula property, making such systems useful in the design of automated reasoning algorithms. However, the downside of the nested sequent paradigm is that a general theory concerning the automated construction of such calculi (as in the labelled setting) is essentially absent, meaning that the construction of nested systems and the confirmation of their properties is usually done on a case-by-case basis. The refinement method connects both paradigms in a fruitful way, by transforming labelled systems into nested (or, refined labelled) systems with the properties of the former preserved throughout the transformation process.
To demonstrate the method of refinement and some of its applications, we consider grammar logics, first-order intuitionistic logics, and deontic STIT logics. The introduced refined labelled calculi will be used to provide the first proof-search algorithms for deontic STIT logics. Furthermore, we employ our refined labelled calculi for grammar logics to show that every logic in the class possesses the effective Lyndon interpolation property.

[3]  arXiv:2107.14651 [pdf, ps, other]
Title: Minimal Translations from Synchronous Communication to Synchronizing Locks (Extended Version)
Subjects: Logic in Computer Science (cs.LO)

In order to understand the relative expressive power of larger concurrent programming languages, we analyze translations of small process calculi which model the communication and synchronization of concurrent processes. The source language SYNCSIMPLE is a minimalistic model for message passing concurrency while the target language LOCKSIMPLE is a minimalistic model for shared memory concurrency. The former is a calculus with synchronous communication of processes, while the latter has synchronizing mutable locations -- called locks -- that behave similarly to binary semaphores. The criteria for correctness of translations is that they preserve and reflect may-termination and must-termination of the processes. We show that there is no correct compositional translation from SYNCSIMPLE to LOCKSIMPLE that uses one or two locks, independent from the initialisation of the locks. We also show that there is a correct translation that uses three locks. Also variants of the locks are taken into account with different blocking behavior.

[4]  arXiv:2107.14668 [pdf, ps, other]
Title: Interleaving & Reconfigurable Interaction: Separating Choice from Scheduling using Glue
Comments: This work is funded by the ERC consolidator grant D-SynMA (No. 772459) and the Swedish research council grants: SynTM (No.2020-03401) and VR project (No. 2020-04963)
Subjects: Logic in Computer Science (cs.LO)

Reconfigurable interaction induces another dimension of nondeterminism in concurrent systems which makes it hard to reason about the different choices of the system from a global perspective. Namely, (1) choices that correspond to concurrent execution of independent events; and (2) forced interleaving (or scheduling) due to reconfiguration. Unlike linear order semantics of computations, partial order semantics recovers information about the interdependence among the different events for fixed interaction, but still is unable to handle reconfiguration. We introduce glued partial orders as a way to capture reconfiguration. Much like partial orders capture all possible choices for fixed systems, glued partial orders capture all possible choices alongside reconfiguration. We show that a glued partial order is sufficient to correctly capture all partial order computations that differ in forced interleaving due to reconfiguration. Furthermore, we show that computations belonging to different glued partial orders are only different due to non-determinism.

Cross-lists for Mon, 2 Aug 21

[5]  arXiv:2107.14325 (cross-list from cs.CR) [pdf]
Title: PiBase: An IoT-based Security System using Raspberry Pi and Google Firebase
Subjects: Cryptography and Security (cs.CR); Computer Vision and Pattern Recognition (cs.CV); Logic in Computer Science (cs.LO)

Smart environments are environments where digital devices are connected to each other over the Internet and operate in sync. Security is of paramount importance in such environments. This paper addresses aspects of authorized access and intruder detection for smart environments. Proposed is PiBase, an Internet of Things (IoT)-based app that aids in detecting intruders and providing security. The hardware for the application consists of a Raspberry Pi, a PIR motion sensor to detect motion from infrared radiation in the environment, an Android mobile phone and a camera. The software for the application is written in Java, Python and NodeJS. The PIR sensor and Pi camera module connected to the Raspberry Pi aid in detecting human intrusion. Machine learning algorithms, namely Haar-feature based cascade classifiers and Linear Binary Pattern Histograms (LBPH), are used for face detection and face recognition, respectively. The app lets the user create a list of non-intruders and anyone that is not on the list is identified as an intruder. The app alerts the user only in the event of an intrusion by using the Google Firebase Cloud Messaging service to trigger a notification to the app. The user may choose to add the detected intruder to the list of non-intruders through the app to avoid further detections as intruder. Face detection by the Haar Cascade algorithm yields a recall of 94.6%. Thus, the system is both highly effective and relatively low cost.

[6]  arXiv:2107.14509 (cross-list from cs.DC) [pdf, other]
Title: On Strong Observational Refinement and Forward Simulation
Comments: Full version of the paper to appear in DISC 2021
Subjects: Distributed, Parallel, and Cluster Computing (cs.DC); Logic in Computer Science (cs.LO)

Hyperproperties are correctness conditions for labelled transition systems that are more expressive than traditional trace properties, with particular relevance to security. Recently, Attiya and Enea studied a notion of strong observational refinement that preserves all hyperproperties. They analyse the correspondence between forward simulation and strong observational refinement in a setting with finite traces only. We study this correspondence in a setting with both finite and infinite traces. In particular, we show that forward simulation does not preserve hyperliveness properties in this setting. We extend the forward simulation proof obligation with a progress condition, and prove that this progressive forward simulation does imply strong observational refinement.

[7]  arXiv:2107.14581 (cross-list from quant-ph) [pdf, ps, other]
Title: Causality in higher order process theories
Subjects: Quantum Physics (quant-ph); Logic in Computer Science (cs.LO); Category Theory (math.CT)

Quantum supermaps provide a framework in which higher order quantum processes can act on lower order quantum processes. In doing so, they enable the definition and analysis of new quantum protocols and causal structures. Recently, the key features of quantum supermaps were captured through a general categorical framework, which when iterated yields the framework of higher order process theories (HOPT). The HOPT framework combines lower and higher order transformations in a single unified theory, with its mathematical structure shown to coincide with the notion of a closed monoidal category. Here we provide an equivalent construction of the HOPT framework from four simple axioms of process-theoretic nature. We then use the HOPT framework to establish connections between foundational features such as causality, determinism, and signalling, and to explore their interaction with the mathematical structure of *-autonomy.

Replacements for Mon, 2 Aug 21

[8]  arXiv:1811.04196 (replaced) [pdf]
Title: A Domain Theory for Statistical Probabilistic Programming
Journal-ref: Proc. ACM Program. Lang. 3(POPL): 36:1-36:29 (2019)
Subjects: Logic in Computer Science (cs.LO); Programming Languages (cs.PL)
[9]  arXiv:2004.11185 (replaced) [pdf, ps, other]
Title: Proof Theory of Riesz Spaces and Modal Riesz Spaces
Subjects: Logic in Computer Science (cs.LO)
[10]  arXiv:2103.05674 (replaced) [pdf, other]
Title: Synthesizing computable functions from rational specifications over infinite words
Subjects: Formal Languages and Automata Theory (cs.FL); Logic in Computer Science (cs.LO)
[11]  arXiv:2105.10362 (replaced) [pdf, other]
Title: Functionals in the Clouds: An abstract architecture of serverless Cloud-Native Apps
Comments: improved version for submission to UCC 2021
Subjects: Computation and Language (cs.CL); Logic in Computer Science (cs.LO)
[ total of 11 entries: 1-11 ]
[ showing up to 2000 entries per page: fewer | more ]

Disable MathJax (What is MathJax?)

Links to: arXiv, form interface, find, cs, recent, 2108, contact, help  (Access key information)