Dagstuhl Publishing
http://www.dagstuhl.de
RSS feed announcing the latest publications published by Schloss Dagstuhlen-en2010-06-082018-06-06http://www.dagstuhl.de/dagpub-rss.phpFront Matter, Table of Contents, Preface, Conference Organization
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=11404
Front Matter, Table of Contents, Preface, Conference OrganizationTue, 19 Nov 2019 00:00:00 +0100http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=11404Martin Hofmann's Case for Non-Strictly Positive Data Types
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=11405
We describe the breadth-first traversal algorithm by Martin Hofmann that uses a non-strictly positive data type and carry out a simple verification in an extensional setting. Termination is shown by implementing the algorithm in the strongly normalising extension of system F by Mendler-style recursion. We then analyze the same algorithm by alternative verifications first in an intensional setting using a non-strictly positive inductive definition (not just a non-strictly positive data type), and subsequently by two different algebraic reductions. The verification approaches are compared in terms of notions of simulation and should elucidate the somewhat mysterious algorithm and thus make a case for other uses of non-strictly positive data types. Except for the termination proof, which cannot be formalised in Coq, all proofs were formalised in Coq and some of the algorithms were implemented in Agda and Haskell.Tue, 19 Nov 2019 00:00:00 +0100http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=11405A Simpler Undecidability Proof for System F Inhabitation
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=11406
Tue, 19 Nov 2019 00:00:00 +0100http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=11406Dependent Sums and Dependent Products in Bishop's Set Theory
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=11407
According to the standard, non type-theoretic accounts of Bishop's constructivism (BISH), dependent functions are not necessary to BISH. Dependent functions though, are explicitly used by Bishop in his definition of the intersection of a family of subsets, and they are necessary to the definition of arbitrary products. In this paper we present the basic notions and principles of CSFT, a semi-formal constructive theory of sets and functions intended to be a minimal, adequate and faithful, in Feferman's sense, semi-formalisation of Bishop's set theory (BST). We define the notions of dependent sum (or exterior union) and dependent product of set-indexed families of sets within CSFT, and we prove the distributivity of prod over sum i.e., the translation of the type-theoretic axiom of choice within CSFT. We also define the notions of dependent sum (or interior union) and dependent product of set-indexed families of subsets within CSFT. For these definitions we extend BST with the universe of sets #1 V_0 and the universe of functions #1 V_1.Tue, 19 Nov 2019 00:00:00 +0100http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=11407Semantic Subtyping for Non-Strict Languages
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=11408
Semantic subtyping is an approach to define subtyping relations for type systems featuring union and intersection type connectives. It has been studied only for strict languages, and it is unsound for non-strict semantics. In this work, we study how to adapt this approach to non-strict languages: in particular, we define a type system using semantic subtyping for a functional language with a call-by-need semantics. We do so by introducing an explicit representation for divergence in the types, so that the type system distinguishes expressions that are results from those which are computations that might diverge.Tue, 19 Nov 2019 00:00:00 +0100http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=11408New Formalized Results on the Meta-Theory of a Paraconsistent Logic
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=11409
Classical logics are explosive, meaning that everything follows from a contradiction. Paraconsistent logics are logics that are not explosive. This paper presents the meta-theory of a paraconsistent infinite-valued logic, in particular new results showing that while the question of validity for a given formula can be reduced to a consideration of only finitely many truth values, this does not mean that the logic collapses to a finite-valued logic. All definitions and theorems are formalized in the Isabelle/HOL proof assistant.Tue, 19 Nov 2019 00:00:00 +0100http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=11409Normalization by Evaluation for Typed Weak lambda-Reduction
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=11410
Tue, 19 Nov 2019 00:00:00 +0100http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=11410Cubical Assemblies, a Univalent and Impredicative Universe and a Failure of Propositional Resizing
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=11411
We construct a model of cubical type theory with a univalent and impredicative universe in a category of cubical assemblies. We show that this impredicative universe in the cubical assembly model does not satisfy a form of propositional resizing.Tue, 19 Nov 2019 00:00:00 +0100http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=11411OASIcs, Volume 73, CERTS'19, Complete Volume
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=11389
OASIcs, Volume 73, CERTS'19, Complete VolumeWed, 30 Oct 2019 08:46:12 +0100http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=11389LIPIcs, Volume 147, TIME'19, Complete Volume
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=11388
LIPIcs, Volume 147, TIME'19, Complete VolumeWed, 30 Oct 2019 08:46:02 +0100http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=11388LIPIcs, Volume 146, DISC'19, Complete Volume
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=11387
LIPIcs, Volume 146, DISC'19, Complete VolumeWed, 30 Oct 2019 08:45:51 +0100http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=11387Control of Networked Cyber-Physical Systems (Dagstuhl Seminar 19222)
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=11384
This report documents the program and the outcomes of Dagstuhl Seminar 19222 "Control of Networked Cyber-Physical Systems".Such systems typically operate under very tight timing constraints and at the same time witness an ever-increasing complexity in both size and the amount of information needed to main controllability.Yet, the development of control systems and of communication/computation infrastructures has traditionally been decoupled, so that valuable insights from the respective other domain could not be used towards the joint goal of keeping cyber-physical systems (CPS) controllable.In order to overcome this "black box" thinking, the seminar brought together researchers from the key communities involved in the development of CPS.In a series of impulse talks and plenary discussions, the seminar reviewed the current start-of-the-art in CPS research and identified promising research directions that may benefit from closer cooperation between the communication and control communities.Mon, 28 Oct 2019 14:24:31 +0100http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=11384Topology, Computation and Data Analysis (Dagstuhl Seminar 19212)
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=11383
This report documents the program and the outcomes of Dagstuhl Seminar 19212 "Topology, Computation and Data Analysis". The seminar brought together researchers with mathematical and computational backgrounds in addressing emerging directions within computational topology for data analysis in practice. This seminar was designed to be a followup event after a very successful Dagstuhl Seminar (17292; July 2017). The list of topics and participants were updated to keep the discussions diverse, refreshing, and engaging. This seminar facilitated close interactions among the attendees with the aim of accelerating the convergence between mathematical and computational thinking in the development of theories and scalable algorithms for data analysis.Mon, 28 Oct 2019 14:24:23 +0100http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=11383Enumeration in Data Management (Dagstuhl Seminar 19211)
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=11382
This report documents the program and the outcomes of Dagstuhl Seminar 19211 "Enumeration in Data Management". The goal of the seminar was to bring together researchers from various fields of computer science, including the Databases, Computational Logic, and Algorithms communities, and establish the means of collaboration towards considerable progress on the topic. Specifically, we aimed at understanding the recent developments, identifying the important open problems, and initiating collaborative efforts towards solutions thereof. In addition, we aimed to build and disseminate a toolkit for data-centric enumeration problems, including algorithmic techniques, proof techniques, and important indicator problems. Towards the objectives, the seminar included tutorials on the topic, invited talks, presentations of open problems, working groups on the open problems, discussions on platforms to compile the community knowledge, and the construction of various skeletons of such compilations.Mon, 28 Oct 2019 14:24:14 +0100http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=11382Approaches and Applications of Inductive Programming (Dagstuhl Seminar 19202)
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=11381
In this report the program and the outcomes of Dagstuhl Seminar 19202 "Approaches and Applications of Inductive Programming" is documented. After a short introduction to the state of the art to inductive programming research, an overview of the introductory tutorials, the talks, program demonstrations, and the outcomes of discussion groups is given.Mon, 28 Oct 2019 14:24:07 +0100http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=11381Visual Analytics for Sets over Time and Space (Dagstuhl Seminar 19192)
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=11380
This report documents the program and the outcomes of Dagstuhl Seminar 19192 "Visual Analytics for Sets over Time and Space", which brought together 29 researchers working on visualization (i) from a theoretical point of view (graph drawing, computational geometry, and cognition), (ii) from a temporal point of view (visual analytics and information visualization over time, HCI), and (iii) from a space-time point of view (cartography, GIScience).The goal of the seminar was to identify specific theoretical and practical problems that need to be solved in order to create dynamic and interactive set visualizations that take into account time and space, and to begin working on these problems.The first 1.5 days were reserved for overview presentations from representatives of the different communities, for presenting open problems, and for forming interdisciplinary working groups that will focus on some of the identified open problems as a group. There were three survey talks, ten short talks, and one panel with three contributors.The remaining three days consisted of open mic sessions, working-group meetings, and progress reports.Five working groups were formed that investigated several of the open research questions. Abstracts of the talks and a report from each working group are included in this report.Mon, 28 Oct 2019 14:24:01 +0100http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=11380Software Evolution in Time and Space: Unifying Version and Variability Management (Dagstuhl Seminar 19191)
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=11379
Effectively managing versions and variants of software systems are among the main challenges of software engineering. Over the last decades, two large research fields, Software Configuration Management (SCM) and Software Product Line Engineering (SPLE), have focused on addressing the version and the variant management, respectively. Yet, large-scale systems require addressing both challenges in a unified way. The SCM community regularly faces the need to support variants, while SPLE needs versioning support. However, neither community has been successful in producing unified version and variant management techniques that are effective in practice. This seminar aimed at establishing a body of knowledge of version and variant management techniques. Together with industrial practitioners, we invited researchers from both fields to conceive an ontology of SCM and SPLE concepts, to identify open problems, and to elicit and synthesize practitioners' challenges and requirements. These outcomes provided the basis to create a research agenda, research infrastructure, and working groups, and finally, to establish a benchmark for evaluating future research results. As such, the seminar enabled research on enhanced version and variant management techniques that will ultimately be adopted in practice.Mon, 28 Oct 2019 14:23:54 +0100http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=11379