eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-06-18
131
0
0
10.4230/LIPIcs.FSCD.2019
article
LIPIcs, Volume 131, FSCD'19, Complete Volume
Geuvers, Herman
1
2
https://orcid.org/0000-0003-2522-2980
Radboud University Nijmegen, The Netherlands
Technical University Eindhoven, The Netherlands
LIPIcs, Volume 131, FSCD'19, Complete Volume
https://drops.dagstuhl.de/storage/00lipics/lipics-vol131-fscd2019/LIPIcs.FSCD.2019/LIPIcs.FSCD.2019.pdf
Theory of computation, Models of computation, Formal languages and automata theory, Logic, Semantics and reasoning
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-06-18
131
0:i
0:xx
10.4230/LIPIcs.FSCD.2019.0
article
Front Matter, Table of Contents, Preface, Conference Organization
Geuvers, Herman
1
2
https://orcid.org/0000-0003-2522-2980
Radboud University Nijmegen, The Netherlands
Technical University Eindhoven, The Netherlands
Front Matter, Table of Contents, Preface, Conference Organization
https://drops.dagstuhl.de/storage/00lipics/lipics-vol131-fscd2019/LIPIcs.FSCD.2019.0/LIPIcs.FSCD.2019.0.pdf
Front Matter
Table of Contents
Preface
Conference Organization
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-06-18
131
1:1
1:20
10.4230/LIPIcs.FSCD.2019.1
article
A Fresh Look at the lambda-Calculus (Invited Talk)
Accattoli, Beniamino
1
Inria & LIX, École Polytechnique, UMR 7161, France
The (untyped) lambda-calculus is almost 90 years old. And yet - we argue here - its study is far from being over. The paper is a bird’s eye view of the questions the author worked on in the last few years: how to measure the complexity of lambda-terms, how to decompose their evaluation, how to implement it, and how all this varies according to the evaluation strategy. The paper aims at inducing a new way of looking at an old topic, focussing on high-level issues and perspectives.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol131-fscd2019/LIPIcs.FSCD.2019.1/LIPIcs.FSCD.2019.1.pdf
lambda-calculus
sharing
abstract machines
type systems
rewriting
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-06-18
131
2:1
2:2
10.4230/LIPIcs.FSCD.2019.2
article
A Linear Logical Framework in Hybrid (Invited Talk)
Felty, Amy P.
1
https://orcid.org/0000-0001-7195-2613
University of Ottawa, Canada
We present a linear logical framework implemented within the Hybrid system [Amy P. Felty and Alberto Momigliano, 2012]. Hybrid is designed to support the use of higher-order abstract syntax for representing and reasoning about formal systems, implemented in the Coq Proof Assistant. In this work, we extend the system with two linear specification logics, which provide infrastructure for reasoning directly about object languages with linear features.
We originally developed this framework in order to address the challenges of reasoning about the type system of a quantum lambda calculus. In particular, we started by considering the Proto-Quipper language [Neil J. Ross, 2015], which contains the core of Quipper [Green et al., 2013; Peter Selinger and Benoît Valiron, 2006]. Quipper is a relatively new quantum programming language under active development with a linear type system. We have completed a formal proof of type soundness for Proto-Quipper [Mohamed Yousri Mahmoud and Amy P. Felty, 2018]. Our current work includes extending this work to other properties of Proto-Quipper, reasoning about other quantum programming languages [Mohamed Yousri Mahmoud and Amy P. Felty, 2018], and reasoning about other languages such as the meta-theory of low-level abstract machine code.
We are also interested in applying this framework to applications outside the domain of meta-theory of programming languages and have focused on two areas - formal reasoning about the proof theory of focused linear sequent calculi and modeling biological processes as transition systems and proving properties about them. We found that a slight extension of the initial linear specification logic allowed us to provide succinct encodings and facilitate reasoning in these new domains. We illustrate by discussing a model of breast cancer progression as a set of transition rules and proving properties about this model [Joëlle Despeyroux et al., 2018]. Current work also includes modeling stem cells as they mature into different types of blood cells.
This work illustrates the use of Hybrid as a meta-logical framework for fast prototyping of logical frameworks, which is achieved by defining inference rules of a specification logic inductively in Coq and building a library of definitions and lemmas used to reason about a class of object logics. Our focus here is on linear specification logics and their applications.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol131-fscd2019/LIPIcs.FSCD.2019.2/LIPIcs.FSCD.2019.2.pdf
Logical frameworks
proof assistants
linear logic
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-06-18
131
3:1
3:15
10.4230/LIPIcs.FSCD.2019.3
article
Extending Maximal Completion (Invited Talk)
Winkler, Sarah
1
https://orcid.org/0000-0001-8114-3107
University of Innsbruck, Austria
Maximal completion (Klein and Hirokawa 2011) is an elegantly simple yet powerful variant of Knuth-Bendix completion. This paper extends the approach to ordered completion and theorem proving as well as normalized completion. An implementation of the different procedures is described, and its practicality is demonstrated by various examples.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol131-fscd2019/LIPIcs.FSCD.2019.3/LIPIcs.FSCD.2019.3.pdf
automated reasoning
completion
theorem proving
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-06-18
131
4:1
4:6
10.4230/LIPIcs.FSCD.2019.4
article
Some Semantic Issues in Probabilistic Programming Languages (Invited Talk)
Yang, Hongseok
1
School of Computing, KAIST, South Korea
This is a slightly extended abstract of my talk at FSCD'19 about probabilistic programming and a few semantic issues on it. The main purpose of this abstract is to provide keywords and references on the work mentioned in my talk, and help interested audience to do follow-up study.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol131-fscd2019/LIPIcs.FSCD.2019.4/LIPIcs.FSCD.2019.4.pdf
Probabilistic Programming
Denotational Semantics
Non-differentiable Models
Bayesian Nonparametrics
Exchangeability
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-06-18
131
5:1
5:17
10.4230/LIPIcs.FSCD.2019.5
article
Bicategories in Univalent Foundations
Ahrens, Benedikt
1
https://orcid.org/0000-0002-6786-4538
Frumin, Dan
2
https://orcid.org/0000-0001-5864-7278
Maggesi, Marco
3
https://orcid.org/0000-0003-4380-7691
van der Weide, Niels
2
https://orcid.org/0000-0003-1146-4161
School of Computer Science, University of Birmingham, United Kingdom
Institute for Computation and Information Sciences, Radboud University, Nijmegen, The Netherlands
Dipartimento di Matematica e Informatica "Dini", Università degli Studi di Firenze, Italy
We develop bicategory theory in univalent foundations. Guided by the notion of univalence for (1-)categories studied by Ahrens, Kapulkin, and Shulman, we define and study univalent bicategories. To construct examples of those, we develop the notion of "displayed bicategories", an analog of displayed 1-categories introduced by Ahrens and Lumsdaine. Displayed bicategories allow us to construct univalent bicategories in a modular fashion. To demonstrate the applicability of this notion, we prove several bicategories are univalent. Among these are the bicategory of univalent categories with families and the bicategory of pseudofunctors between univalent bicategories. Our work is formalized in the UniMath library of univalent mathematics.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol131-fscd2019/LIPIcs.FSCD.2019.5/LIPIcs.FSCD.2019.5.pdf
bicategory theory
univalent mathematics
dependent type theory
Coq
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-06-18
131
6:1
6:19
10.4230/LIPIcs.FSCD.2019.6
article
Modular Specification of Monads Through Higher-Order Presentations
Ahrens, Benedikt
1
https://orcid.org/0000-0002-6786-4538
Hirschowitz, André
2
https://orcid.org/0000-0003-2523-1481
Lafont, Ambroise
3
https://orcid.org/0000-0002-9299-641X
Maggesi, Marco
4
https://orcid.org/0000-0003-4380-7691
University of Birmingham, United Kingdom
Université Côte d'Azur, CNRS, LJAD, Nice, France
IMT Atlantique, Inria, LS2N CNRS, Nantes, France
Università degli Studi di Firenze, Italy
In their work on second-order equational logic, Fiore and Hur have studied presentations of simply typed languages by generating binding constructions and equations among them. To each pair consisting of a binding signature and a set of equations, they associate a category of "models", and they give a monadicity result which implies that this category has an initial object, which is the language presented by the pair.
In the present work, we propose, for the untyped setting, a variant of their approach where monads and modules over them are the central notions. More precisely, we study, for monads over sets, presentations by generating ("higher-order") operations and equations among them. We consider a notion of 2-signature which allows to specify a monad with a family of binding operations subject to a family of equations, as is the case for the paradigmatic example of the lambda calculus, specified by its two standard constructions (application and abstraction) subject to beta- and eta-equalities. Such a 2-signature is hence a pair (Sigma,E) of a binding signature Sigma and a family E of equations for Sigma. This notion of 2-signature has been introduced earlier by Ahrens in a slightly different context.
We associate, to each 2-signature (Sigma,E), a category of "models of (Sigma,E)"; and we say that a 2-signature is "effective" if this category has an initial object; the monad underlying this (essentially unique) object is the "monad specified by the 2-signature". Not every 2-signature is effective; we identify a class of 2-signatures, which we call "algebraic", that are effective.
Importantly, our 2-signatures together with their models enjoy "modularity": when we glue (algebraic) 2-signatures together, their initial models are glued accordingly.
We provide a computer formalization for our main results.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol131-fscd2019/LIPIcs.FSCD.2019.6/LIPIcs.FSCD.2019.6.pdf
free monads
presentation of monads
initial semantics
signatures
syntax
monadic substitution
computer-checked proofs
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-06-18
131
7:1
7:21
10.4230/LIPIcs.FSCD.2019.7
article
Towards the Average-Case Analysis of Substitution Resolution in Lambda-Calculus
Bendkowski, Maciej
1
Jagiellonian University, Faculty of Mathematics and Computer Science, Theoretical Computer Science Department, ul. Prof. Łojasiewicza 6, 30 - 348 Kraków, Poland
Substitution resolution supports the computational character of beta-reduction, complementing its execution with a capture-avoiding exchange of terms for bound variables. Alas, the meta-level definition of substitution, masking a non-trivial computation, turns beta-reduction into an atomic rewriting rule, despite its varying operational complexity. In the current paper we propose a somewhat indirect average-case analysis of substitution resolution in the classic lambda-calculus, based on the quantitative analysis of substitution in lambda-upsilon, an extension of lambda-calculus internalising the upsilon-calculus of explicit substitutions. Within this framework, we show that for any fixed n >= 0, the probability that a uniformly random, conditioned on size, lambda-upsilon-term upsilon-normalises in n normal-order (i.e. leftmost-outermost) reduction steps tends to a computable limit as the term size tends to infinity. For that purpose, we establish an effective hierarchy (G_n)_n of regular tree grammars partitioning upsilon-normalisable terms into classes of terms normalising in n normal-order rewriting steps. The main technical ingredient in our construction is an inductive approach to the construction of G_{n+1} out of G_n based, in turn, on the algorithmic construction of finite intersection partitions, inspired by Robinson’s unification algorithm. Finally, we briefly discuss applications of our approach to other term rewriting systems, focusing on two closely related formalisms, i.e. the full lambda-upsilon-calculus and combinatory logic.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol131-fscd2019/LIPIcs.FSCD.2019.7/LIPIcs.FSCD.2019.7.pdf
lambda calculus
explicit substitutions
complexity
combinatorics
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-06-18
131
8:1
8:20
10.4230/LIPIcs.FSCD.2019.8
article
Deriving an Abstract Machine for Strong Call by Need
Biernacka, Małgorzata
1
Charatonik, Witold
1
Institute of Computer Science, University of Wrocław, Poland
Strong call by need is a reduction strategy for computing strong normal forms in the lambda calculus, where terms are fully normalized inside the bodies of lambda abstractions and open terms are allowed. As typical for a call-by-need strategy, the arguments of a function call are evaluated at most once, only when they are needed. This strategy has been introduced recently by Balabonski et al., who proved it complete with respect to full beta-reduction and conservative over weak call by need.
We show a novel reduction semantics and the first abstract machine for the strong call-by-need strategy. The reduction semantics incorporates syntactic distinction between strict and non-strict let constructs and is geared towards an efficient implementation. It has been defined within the framework of generalized refocusing, i.e., a generic method that allows to go from a reduction semantics instrumented with context kinds to the corresponding abstract machine; the machine is thus correct by construction. The format of the semantics that we use makes it explicit that strong call by need is an example of a hybrid strategy with an infinite number of substrategies.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol131-fscd2019/LIPIcs.FSCD.2019.8/LIPIcs.FSCD.2019.8.pdf
abstract machines
reduction semantics
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-06-18
131
9:1
9:21
10.4230/LIPIcs.FSCD.2019.9
article
Dependency Pairs Termination in Dependent Type Theory Modulo Rewriting
Blanqui, Frédéric
1
2
Genestier, Guillaume
2
3
Hermant, Olivier
3
INRIA, France
LSV, ENS Paris-Saclay, CNRS, Université Paris-Saclay, France
MINES ParisTech, PSL University, Paris, France
Dependency pairs are a key concept at the core of modern automated termination provers for first-order term rewriting systems. In this paper, we introduce an extension of this technique for a large class of dependently-typed higher-order rewriting systems. This extends previous results by Wahlstedt on the one hand and the first author on the other hand to strong normalization and non-orthogonal rewriting systems. This new criterion is implemented in the type-checker Dedukti.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol131-fscd2019/LIPIcs.FSCD.2019.9/LIPIcs.FSCD.2019.9.pdf
termination
higher-order rewriting
dependent types
dependency pairs
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-06-18
131
10:1
10:19
10.4230/LIPIcs.FSCD.2019.10
article
A Generic Framework for Higher-Order Generalizations
Cerna, David M.
1
Kutsia, Temur
2
FMV and RISC, Johannes Kepler University Linz, Austria
RISC, Johannes Kepler University Linz, Austria
We consider a generic framework for anti-unification of simply typed lambda terms. It helps to compute generalizations which contain maximally common top part of the input expressions, without nesting generalization variables. The rules of the corresponding anti-unification algorithm are formulated, and their soundness and termination are proved. The algorithm depends on a parameter which decides how to choose terms under generalization variables. Changing the particular values of the parameter, we obtained four new unitary variants of higher-order anti-unification and also showed how the already known pattern generalization fits into the schema.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol131-fscd2019/LIPIcs.FSCD.2019.10/LIPIcs.FSCD.2019.10.pdf
anti-unification
typed lambda calculus
least general generalization
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-06-18
131
11:1
11:23
10.4230/LIPIcs.FSCD.2019.11
article
Homotopy Canonicity for Cubical Type Theory
Coquand, Thierry
1
Huber, Simon
1
Sattler, Christian
1
Department of Computer Science and Engineering, University of Gothenburg, Sweden
Cubical type theory provides a constructive justification of homotopy type theory and satisfies canonicity: every natural number is convertible to a numeral. A crucial ingredient of cubical type theory is a path lifting operation which is explained computationally by induction on the type involving several non-canonical choices. In this paper we show by a sconing argument that if we remove these equations for the path lifting operation from the system, we still retain homotopy canonicity: every natural number is path equal to a numeral.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol131-fscd2019/LIPIcs.FSCD.2019.11/LIPIcs.FSCD.2019.11.pdf
cubical type theory
univalence
canonicity
sconing
Artin glueing
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-06-18
131
12:1
12:18
10.4230/LIPIcs.FSCD.2019.12
article
Polymorphic Higher-Order Termination
Czajka, Łukasz
1
https://orcid.org/0000-0001-8083-4280
Kop, Cynthia
2
https://orcid.org/0000-0002-6337-2544
Faculty of Informatics, TU Dortmund, Germany
Institute of Computer Science, Radboud University Nijmegen, The Netherlands
We generalise the termination method of higher-order polynomial interpretations to a setting with impredicative polymorphism. Instead of using weakly monotonic functionals, we interpret terms in a suitable extension of System F_omega. This enables a direct interpretation of rewrite rules which make essential use of impredicative polymorphism. In addition, our generalisation eases the applicability of the method in the non-polymorphic setting by allowing for the encoding of inductive data types. As an illustration of the potential of our method, we prove termination of a substantial fragment of full intuitionistic second-order propositional logic with permutative conversions.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol131-fscd2019/LIPIcs.FSCD.2019.12/LIPIcs.FSCD.2019.12.pdf
termination
polymorphism
higher-order rewriting
permutative conversions
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-06-18
131
13:1
13:16
10.4230/LIPIcs.FSCD.2019.13
article
On the Taylor Expansion of Probabilistic lambda-terms
Dal Lago, Ugo
1
2
Leventis, Thomas
2
University of Bologna, Italy
INRIA Sophia Antipolis, France
We generalise Ehrhard and Regnier’s Taylor expansion from pure to probabilistic lambda-terms. We prove that the Taylor expansion is adequate when seen as a way to give semantics to probabilistic lambda-terms, and that there is a precise correspondence with probabilistic Böhm trees, as introduced by the second author. We prove this adequacy through notions of probabilistic resource terms and explicit Taylor expansion.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol131-fscd2019/LIPIcs.FSCD.2019.13/LIPIcs.FSCD.2019.13.pdf
Probabilistic Lambda-Calculi
Taylor Expansion
Linear Logic
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-06-18
131
14:1
14:23
10.4230/LIPIcs.FSCD.2019.14
article
Proof Normalisation in a Logic Identifying Isomorphic Propositions
Díaz-Caro, Alejandro
1
2
https://orcid.org/0000-0002-5175-6882
Dowek, Gilles
3
https://orcid.org/0000-0001-6253-935X
Instituto de Ciencias de la Computación (CONICET-Universidad de Buenos Aires), Ciudad Autónoma de Buenos Aires, Argentina
Universidad Nacional de Quilmes, Bernal (Buenos Aires), Argentina
Inria, LSV, ENS Paris-Saclay, France
We define a fragment of propositional logic where isomorphic propositions, such as A wedge B and B wedge A, or A ==> (B wedge C) and (A ==> B) wedge (A ==> C) are identified. We define System I, a proof language for this logic, and prove its normalisation and consistency.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol131-fscd2019/LIPIcs.FSCD.2019.14/LIPIcs.FSCD.2019.14.pdf
Simply typed lambda calculus
Isomorphisms
Logic
Cut-elimination
Proof-reduction
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-06-18
131
15:1
15:16
10.4230/LIPIcs.FSCD.2019.15
article
lambda!-calculus, Intersection Types, and Involutions
Ciaffaglione, Alberto
1
Di Gianantonio, Pietro
1
Honsell, Furio
1
Lenisa, Marina
1
Scagnetto, Ivan
1
Department of Mathematics, Computer Science and Physics, University of Udine, Italy
Abramsky’s affine combinatory algebras are models of affine combinatory logic, which refines standard combinatory logic in the direction of Linear Logic. Abramsky introduced various universal models of computation based on affine combinatory algebras, consisting of partial involutions over a suitable formal language {of moves}, in order to discuss reversible computation in a Geometry of Interaction setting. We investigate partial involutions from the point of view of the model theory of lambda!-calculus. The latter is a refinement of the standard lambda-calculus, corresponding to affine combinatory logic. We introduce intersection type systems for the lambda!-calculus, by extending standard intersection types with a !_u-operator. These induce affine combinatory algebras, and, via suitable quotients, models of the lambda!-calculus. In particular, we introduce an intersection type system for assigning principal types to lambda!-terms, and we state a correspondence between the partial involution interpreting a combinator and the principal type of the corresponding lambda!-term. This analogy allows for explaining as unification between principal types the somewhat awkward linear application of involutions arising from Geometry of Interaction.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol131-fscd2019/LIPIcs.FSCD.2019.15/LIPIcs.FSCD.2019.15.pdf
Affine Combinatory Algebra
Affine Lambda-calculus
Intersection Types
Geometry of Interaction
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-06-18
131
16:1
16:19
10.4230/LIPIcs.FSCD.2019.16
article
Template Games, Simple Games, and Day Convolution
Eberhart, Clovis
1
Hirschowitz, Tom
2
Laouar, Alexis
2
National Institute of Informatics, Tokyo, Japan
Univ. Grenoble Alpes, Univ. Savoie Mont Blanc, CNRS, LAMA, 73000, Chambéry, France
Template games [P.-A. Melliès, 2019] unify various approaches to game semantics, by exhibiting them as instances of a double-categorical variant of the slice construction. However, in the particular case of simple games [R. Harmer et al., 2007; C. Jacq and P.-A. Melliès, 2018], template games do not quite yield the standard (bi)category. We refine the construction using factorisation systems, obtaining as an instance a slight generalisation of simple games and strategies. This proves that template games have the descriptive power to capture combinatorial constraints defining well-known classes of games. Another instance is Day’s convolution monoidal structure on the category of presheaves over a strict monoidal category [B. Day, 1970], which answers a question raised in [C. Eberhart, 2018].
https://drops.dagstuhl.de/storage/00lipics/lipics-vol131-fscd2019/LIPIcs.FSCD.2019.16/LIPIcs.FSCD.2019.16.pdf
Game semantics
Day convolution
Categorical semantics
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-06-18
131
17:1
17:17
10.4230/LIPIcs.FSCD.2019.17
article
Differentials and Distances in Probabilistic Coherence Spaces
Ehrhard, Thomas
1
https://orcid.org/0000-0001-5231-5504
CNRS, IRIF, Université de Paris, France
In probabilistic coherence spaces, a denotational model of probabilistic functional languages, morphisms are analytic and therefore smooth. We explore two related applications of the corresponding derivatives. First we show how derivatives allow to compute the expectation of execution time in the weak head reduction of probabilistic PCF (pPCF). Next we apply a general notion of "local" differential of morphisms to the proof of a Lipschitz property of these morphisms allowing in turn to relate the observational distance on pPCF terms to a distance the model is naturally equipped with. This suggests that extending probabilistic programming languages with derivatives, in the spirit of the differential lambda-calculus, could be quite meaningful.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol131-fscd2019/LIPIcs.FSCD.2019.17/LIPIcs.FSCD.2019.17.pdf
Denotational semantics
probabilistic coherence spaces
differentials of programs
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-06-18
131
18:1
18:20
10.4230/LIPIcs.FSCD.2019.18
article
Modal Embeddings and Calling Paradigms
Espírito Santo, José
1
https://orcid.org/0000-0002-6348-5653
Pinto, Luís
1
https://orcid.org/0000-0003-1338-2688
Uustalu, Tarmo
2
3
https://orcid.org/0000-0002-1297-0579
Centre of Mathematics, University of Minho, Portugal
School of Computer Science, Reykjavik University, Iceland
Dept. of Software Science, Tallinn University of Technology, Estonia
We study the computational interpretation of the two standard modal embeddings, usually named after Girard and Gödel, of intuitionistic logic into IS4. As source system we take either the call-by-name (cbn) or the call-by-value (cbv) lambda-calculus with simple types. The target system can be taken to be the, arguably, simplest fragment of IS4, here recast as a very simple lambda-calculus equipped with an indeterminate lax monoidal comonad. A slight refinement of the target and of the embeddings shows that: the target is a calculus indifferent to the calling paradigms cbn/cbv, obeying a new paradigm that we baptize call-by-box (cbb), and enjoying standardization; and that Girard’s (resp. Gödel’s) embbedding is a translation of cbn (resp. cbv) lambda-calculus into this calculus, using a compilation technique we call protecting-by-a-box, enjoying the preservation and reflection properties known for cps translations - but in a stronger form that allows the extraction of standardization for cbn or cbv as consequence of standardization for cbb. The modal target and embeddings achieve thus an unification of call-by-name and call-by-value as call-by-box.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol131-fscd2019/LIPIcs.FSCD.2019.18/LIPIcs.FSCD.2019.18.pdf
intuitionistic S4
call-by-name
call-by-value
comonadic lambda-calculus
standardization
indifference property
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-06-18
131
19:1
19:25
10.4230/LIPIcs.FSCD.2019.19
article
Probabilistic Rewriting: Normalization, Termination, and Unique Normal Forms
Faggian, Claudia
1
Université de Paris, IRIF, CNRS, F-75013 Paris, France
While a mature body of work supports the study of rewriting systems, abstract tools for Probabilistic Rewriting are still limited. We study in this setting questions such as uniqueness of the result (unique limit distribution) and normalizing strategies (is there a strategy to find a result with greatest probability?). The goal is to have tools to analyse the operational properties of probabilistic calculi (such as probabilistic lambda-calculi) whose evaluation is also non-deterministic, in the sense that different reductions are possible.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol131-fscd2019/LIPIcs.FSCD.2019.19/LIPIcs.FSCD.2019.19.pdf
probabilistic rewriting
PARS
abstract rewriting systems
confluence
probabilistic lambda calculus
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-06-18
131
20:1
20:24
10.4230/LIPIcs.FSCD.2019.20
article
A Linear-Logical Reconstruction of Intuitionistic Modal Logic S4
Fukuda, Yosuke
1
Yoshimizu, Akira
2
Graduate School of Informatics, Kyoto University, Japan
French Institute for Research in Computer Science and Automation (INRIA), France
We propose a modal linear logic to reformulate intuitionistic modal logic S4 (IS4) in terms of linear logic, establishing an S4-version of Girard translation from IS4 to it. While the Girard translation from intuitionistic logic to linear logic is well-known, its extension to modal logic is non-trivial since a naive combination of the S4 modality and the exponential modality causes an undesirable interaction between the two modalities. To solve the problem, we introduce an extension of intuitionistic multiplicative exponential linear logic with a modality combining the S4 modality and the exponential modality, and show that it admits a sound translation from IS4. Through the Curry-Howard correspondence we further obtain a Geometry of Interaction Machine semantics of the modal lambda-calculus by Pfenning and Davies for staged computation.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol131-fscd2019/LIPIcs.FSCD.2019.20/LIPIcs.FSCD.2019.20.pdf
linear logic
modal logic
Girard translation
Curry-Howard correspondence
geometry of interaction
staged computation
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-06-18
131
21:1
21:21
10.4230/LIPIcs.FSCD.2019.21
article
Sparse Tiling Through Overlap Closures for Termination of String Rewriting
Geser, Alfons
1
Hofbauer, Dieter
2
Waldmann, Johannes
1
HTWK Leipzig, Germany
ASW - Berufsakademie Saarland, Germany
A strictly locally testable language is characterized by its set of admissible factors, prefixes and suffixes, called tiles. We over-approximate reachability sets in string rewriting by languages defined by sparse sets of tiles, containing only those that are reachable in derivations. Using the partial algebra defined by a tiling for semantic labeling, we obtain a transformational method for proving local termination. These algebras can be represented efficiently as finite automata of a certain shape. Using a known result on forward closures, and a new characterisation of overlap closures, we can automatically prove termination and relative termination, respectively. We report on experiments showing the strength of the method.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol131-fscd2019/LIPIcs.FSCD.2019.21/LIPIcs.FSCD.2019.21.pdf
relative termination
semantic labeling
locally testable language
overlap closure
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-06-18
131
22:1
22:22
10.4230/LIPIcs.FSCD.2019.22
article
Proof Nets for First-Order Additive Linear Logic
Heijltjes, Willem B.
1
Hughes, Dominic J. D.
2
Straßburger, Lutz
3
4
University of Bath, United Kingdom
Logic Group, UC Berkeley, USA
Inria Saclay, Palaiseau, France
LIX, École Polytechnique, Palaiseau, France
We present canonical proof nets for first-order additive linear logic, the fragment of linear logic with sum, product, and first-order universal and existential quantification. We present two versions of our proof nets. One, witness nets, retains explicit witnessing information to existential quantification. For the other, unification nets, this information is absent but can be reconstructed through unification. Unification nets embody a central contribution of the paper: first-order witness information can be left implicit, and reconstructed as needed. Witness nets are canonical for first-order additive sequent calculus. Unification nets in addition factor out any inessential choice for existential witnesses. Both notions of proof net are defined through coalescence, an additive counterpart to multiplicative contractibility, and for witness nets an additional geometric correctness criterion is provided. Both capture sequent calculus cut-elimination as a one-step global composition operation.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol131-fscd2019/LIPIcs.FSCD.2019.22/LIPIcs.FSCD.2019.22.pdf
linear logic
first-order logic
proof nets
Herbrand’s theorem
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-06-18
131
23:1
23:16
10.4230/LIPIcs.FSCD.2019.23
article
The Sub-Additives: A Proof Theory for Probabilistic Choice extending Linear Logic
Horne, Ross
1
https://orcid.org/0000-0003-0162-1901
Computer Science and Communications, University of Luxembourg, Esch-sur-Alzette, Luxembourg
Probabilistic choice, where each branch of a choice is weighted according to a probability distribution, is an established approach for modelling processes, quantifying uncertainty in the environment and other sources of randomness. This paper uncovers new insight showing probabilistic choice has a purely logical interpretation as an operator in an extension of linear logic. By forbidding projection and injection, we reveal additive operators between the standard with and plus operators of linear logic. We call these operators the sub-additives. The attention of the reader is drawn to two sub-additive operators: the first being sound with respect to probabilistic choice; while the second arises due to the fact that probabilistic choice cannot be self-dual, hence has a de Morgan dual counterpart. The proof theoretic justification for the sub-additives is a cut elimination result, employing a technique called decomposition. The justification from the perspective of modelling probabilistic concurrent processes is that implication is sound with respect to established notions of probabilistic refinement, and is fully compositional.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol131-fscd2019/LIPIcs.FSCD.2019.23/LIPIcs.FSCD.2019.23.pdf
calculus of structures
probabilistic choice
probabilistic refinement
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-06-18
131
24:1
24:18
10.4230/LIPIcs.FSCD.2019.24
article
A Lower Bound of the Number of Rewrite Rules Obtained by Homological Methods
Ikebuchi, Mirai
1
Massachusetts Institute of Technology, Computer Science and Artificial Intelligence Laboratory, Cambridge, USA
It is well-known that some equational theories such as groups or boolean algebras can be defined by fewer equational axioms than the original axioms. However, it is not easy to determine if a given set of axioms is the smallest or not. Malbos and Mimram investigated a general method to find a lower bound of the cardinality of the set of equational axioms (or rewrite rules) that is equivalent to a given equational theory (or term rewriting systems), using homological algebra. Their method is an analog of Squier’s homology theory on string rewriting systems. In this paper, we develop the homology theory for term rewriting systems more and provide a better lower bound under a stronger notion of equivalence than their equivalence. The author also implemented a program to compute the lower bounds.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol131-fscd2019/LIPIcs.FSCD.2019.24/LIPIcs.FSCD.2019.24.pdf
Term rewriting systems
Equational logic
Homological algebra
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-06-18
131
25:1
25:19
10.4230/LIPIcs.FSCD.2019.25
article
Gluing for Type Theory
Kaposi, Ambrus
1
https://orcid.org/0000-0001-9897-8936
Huber, Simon
2
Sattler, Christian
2
Eötvös Loránd University, Budapest, Hungary
University of Gothenburg, Sweden
The relationship between categorical gluing and proofs using the logical relation technique is folklore. In this paper we work out this relationship for Martin-Löf type theory and show that parametricity and canonicity arise as special cases of gluing. The input of gluing is two models of type theory and a pseudomorphism between them and the output is a displayed model over the first model. A pseudomorphism preserves the categorical structure strictly, the empty context and context extension up to isomorphism, and there are no conditions on preservation of type formers. We look at three examples of pseudomorphisms: the identity on the syntax, the interpretation into the set model and the global section functor. Gluing along these result in syntactic parametricity, semantic parametricity and canonicity, respectively.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol131-fscd2019/LIPIcs.FSCD.2019.25/LIPIcs.FSCD.2019.25.pdf
Martin-Löf type theory
logical relations
parametricity
canonicity
quotient inductive types
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-06-18
131
26:1
26:20
10.4230/LIPIcs.FSCD.2019.26
article
The Discriminating Power of the Let-In Operator in the Lazy Call-by-Name Probabilistic lambda-Calculus
Kašterović, Simona
1
Pagani, Michele
2
Faculty of Technical Sciences, University of Novi Sad , Trg Dositeja Obradovića 6, 21000 Novi Sad, Serbia
IRIF, University Paris Diderot - Paris 7, France
We consider the notion of probabilistic applicative bisimilarity (PAB), recently introduced as a behavioural equivalence over a probabilistic extension of the untyped lambda-calculus. Alberti, Dal Lago and Sangiorgi have shown that PAB is not fully abstract with respect to the context equivalence induced by the lazy call-by-name evaluation strategy. We prove that extending this calculus with a let-in operator allows for achieving the full abstraction. In particular, we recall Larsen and Skou’s testing language, which is known to correspond with PAB, and we prove that every test is representable by a context of our calculus.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol131-fscd2019/LIPIcs.FSCD.2019.26/LIPIcs.FSCD.2019.26.pdf
probabilistic lambda calculus
bisimulation
Howe’s technique
context equivalence
testing
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-06-18
131
27:1
27:20
10.4230/LIPIcs.FSCD.2019.27
article
Hilbert’s Tenth Problem in Coq
Larchey-Wendling, Dominique
1
https://orcid.org/0000-0001-9860-7203
Forster, Yannick
2
Université de Lorraine, CNRS, LORIA, Vandœuvre-lès-Nancy, France
Saarland University, Saarland Informatics Campus, Saarbrücken, Germany
We formalise the undecidability of solvability of Diophantine equations, i.e. polynomial equations over natural numbers, in Coq’s constructive type theory. To do so, we give the first full mechanisation of the Davis-Putnam-Robinson-Matiyasevich theorem, stating that every recursively enumerable problem - in our case by a Minsky machine - is Diophantine. We obtain an elegant and comprehensible proof by using a synthetic approach to computability and by introducing Conway’s FRACTRAN language as intermediate layer.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol131-fscd2019/LIPIcs.FSCD.2019.27/LIPIcs.FSCD.2019.27.pdf
Hilbert’s tenth problem
Diophantine equations
undecidability
computability theory
reduction
Minsky machines
Fractran
Coq
type theory
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-06-18
131
28:1
28:20
10.4230/LIPIcs.FSCD.2019.28
article
The Delta-calculus: Syntax and Types
Liquori, Luigi
1
Stolze, Claude
1
Université Côte d'Azur, Inria, Sophia Antipolis, France
We present the Delta-calculus, an explicitly typed lambda-calculus with strong pairs, projections and explicit type coercions. The calculus can be parametrized with different intersection type theories T, e.g. the Coppo-Dezani, the Coppo-Dezani-Sallé, the Coppo-Dezani-Venneri and the Barendregt-Coppo-Dezani ones, producing a family of Delta-calculi with related intersection typed systems. We prove the main properties like Church-Rosser, unicity of type, subject reduction, strong normalization, decidability of type checking and type reconstruction. We state the relationship between the intersection type assignment systems à la Curry and the corresponding intersection typed systems à la Church by means of an essence function translating an explicitly typed Delta-term into a pure lambda-term one. We finally translate a Delta-term with type coercions into an equivalent one without them; the translation is proved to be coherent because its essence is the identity. The generic Delta-calculus can be parametrized to take into account other intersection type theories as the ones in the Barendregt et al. book.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol131-fscd2019/LIPIcs.FSCD.2019.28/LIPIcs.FSCD.2019.28.pdf
intersection types
lambda calculus à la Church and à la Curry
proof-functional logics
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-06-18
131
29:1
29:18
10.4230/LIPIcs.FSCD.2019.29
article
Pointers in Recursion: Exploring the Tropics
Jacobé de Naurois, Paulin
1
CNRS, Université Paris 13, Sorbonne Paris Cité, LIPN, UMR 7030, F-93430 Villetaneuse, France
We translate the usual class of partial/primitive recursive functions to a pointer recursion framework, accessing actual input values via a pointer reading unit-cost function. These pointer recursive functions classes are proven equivalent to the usual partial/primitive recursive functions. Complexity-wise, this framework captures in a streamlined way most of the relevant sub-polynomial classes. Pointer recursion with the safe/normal tiering discipline of Bellantoni and Cook corresponds to polylogtime computation. We introduce a new, non-size increasing tiering discipline, called tropical tiering. Tropical tiering and pointer recursion, used with some of the most common recursion schemes, capture the classes logspace, logspace/polylogtime, ptime, and NC. Finally, in a fashion reminiscent of the safe recursive functions, tropical tiering is expressed directly in the syntax of the function algebras, yielding the tropical recursive function algebras.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol131-fscd2019/LIPIcs.FSCD.2019.29/LIPIcs.FSCD.2019.29.pdf
Implicit Complexity
Recursion Theory
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-06-18
131
30:1
30:16
10.4230/LIPIcs.FSCD.2019.30
article
Typed Equivalence of Effect Handlers and Delimited Control
Piróg, Maciej
1
https://orcid.org/0000-0002-5889-3388
Polesiuk, Piotr
1
https://orcid.org/0000-0002-7012-4346
Sieczkowski, Filip
1
https://orcid.org/0000-0001-5011-3458
University of Wrocław, Poland
It is folklore that effect handlers and delimited control operators are closely related: recently, this relationship has been proved in an untyped setting for deep handlers and the shift_0 delimited control operator. We positively resolve the conjecture that in an appropriately polymorphic type system this relationship can be extended to the level of types, by identifying the necessary forms of polymorphism, thus extending the definability result to the typed context. In the process, we identify a novel and potentially interesting type system feature for delimited control operators. Moreover, we extend these results to substantiate the folklore connection between shallow handlers and control_0 flavour of delimited control, both in an untyped and typed settings.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol131-fscd2019/LIPIcs.FSCD.2019.30/LIPIcs.FSCD.2019.30.pdf
type-and-effect systems
algebraic effects
delimited control
macro expressibility
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-06-18
131
31:1
31:25
10.4230/LIPIcs.FSCD.2019.31
article
Cubical Syntax for Reflection-Free Extensional Equality
Sterling, Jonathan
1
https://orcid.org/0000-0002-0585-5564
Angiuli, Carlo
1
https://orcid.org/0000-0002-9590-3303
Gratzer, Daniel
2
https://orcid.org/0000-0003-1944-0789
Carnegie Mellon University, Pittsburgh, USA
Aarhus University, Denmark
We contribute XTT, a cubical reconstruction of Observational Type Theory [Altenkirch et al., 2007] which extends Martin-Löf’s intensional type theory with a dependent equality type that enjoys function extensionality and a judgmental version of the unicity of identity proofs principle (UIP): any two elements of the same equality type are judgmentally equal. Moreover, we conjecture that the typing relation can be decided in a practical way. In this paper, we establish an algebraic canonicity theorem using a novel extension of the logical families or categorical gluing argument inspired by Coquand and Shulman [Coquand, 2018; Shulman, 2015]: every closed element of boolean type is derivably equal to either true or false.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol131-fscd2019/LIPIcs.FSCD.2019.31/LIPIcs.FSCD.2019.31.pdf
Dependent type theory
extensional equality
cubical type theory
categorical gluing
canonicity
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-06-18
131
32:1
32:19
10.4230/LIPIcs.FSCD.2019.32
article
Guarded Recursion in Agda via Sized Types
Veltri, Niccolò
1
https://orcid.org/0000-0002-7230-3436
van der Weide, Niels
2
https://orcid.org/0000-0003-1146-4161
Department of Computer Science, IT University of Copenhagen, Denmark
Institute for Computation and Information Sciences, Radboud University, Nijmegen, The Netherlands
In type theory, programming and reasoning with possibly non-terminating programs and potentially infinite objects is achieved using coinductive types. Recursively defined programs of these types need to be productive to guarantee the consistency of the type system. Proof assistants such as Agda and Coq traditionally employ strict syntactic productivity checks, which often make programming with coinductive types convoluted. One way to overcome this issue is by encoding productivity at the level of types so that the type system forbids the implementation of non-productive corecursive programs. In this paper we compare two different approaches to type-based productivity: guarded recursion and sized types. More specifically, we show how to simulate guarded recursion in Agda using sized types. We formalize the syntax of a simple type theory for guarded recursion, which is a variant of Atkey and McBride’s calculus for productive coprogramming. Then we give a denotational semantics using presheaves over the preorder of sizes. Sized types are fundamentally used to interpret the characteristic features of guarded recursion, notably the fixpoint combinator.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol131-fscd2019/LIPIcs.FSCD.2019.32/LIPIcs.FSCD.2019.32.pdf
guarded recursion
type theory
semantics
coinduction
sized types
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-06-18
131
33:1
33:15
10.4230/LIPIcs.FSCD.2019.33
article
Sequence Types for Hereditary Permutators
Vial, Pierre
1
Inria, Nantes, France
The invertible terms in Scott’s model D_infty are known as the hereditary permutators. Equivalently, they are terms which are invertible up to beta eta-conversion with respect to the composition of the lambda-terms. Finding a type-theoretic characterization to the set of hereditary permutators was problem # 20 of TLCA list of problems. In 2008, Tatsuta proved that this was not possible with an inductive type system. Building on previous work, we use an infinitary intersection type system based on sequences (i.e., families of types indexed by integers) to characterize hereditary permutators with a unique type. This gives a positive answer to the problem in the coinductive case.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol131-fscd2019/LIPIcs.FSCD.2019.33/LIPIcs.FSCD.2019.33.pdf
hereditary permutators
Böhm trees
intersection types
coinduction
ridigity
sequence types
non-idempotent intersection
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2019-06-18
131
34:1
34:18
10.4230/LIPIcs.FSCD.2019.34
article
Model Checking Strategy-Controlled Rewriting Systems (System Description)
Rubio, Rubén
1
https://orcid.org/0000-0003-2983-3404
Martí-Oliet, Narciso
1
https://orcid.org/0000-0002-6576-762X
Pita, Isabel
1
https://orcid.org/0000-0003-4915-5452
Verdejo, Alberto
1
https://orcid.org/0000-0002-7374-3214
Facultad de Informática, Universidad Complutense de Madrid, Spain
Strategies are widespread in Computer Science. In the domain of reduction and rewriting systems, strategies are studied as recipes to restrict and control reduction steps and rule applications, which are intimately local, in a derivation-global sense. This idea has been exploited by various tools and rewriting-based specification languages, where strategies are an additional specification layer. Systems so described need to be analyzed too. This article discusses model checking of systems controlled by strategies and presents a working strategy-aware LTL model checker for the Maude specification language, based on rewriting logic, and its strategy language.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol131-fscd2019/LIPIcs.FSCD.2019.34/LIPIcs.FSCD.2019.34.pdf
Model checking
strategies
Maude
rewriting logic