Welcome to WordPress. This is your first post. Edit or delete it, then start writing!
by fscdeuadmin | Oct 9, 2018 | Uncategorized | 0 comments
Welcome to WordPress. This is your first post. Edit or delete it, then start writing!
Title:
Model checking strategy-controlled rewriting systems (Download paper)
Abstract:
Strategies are a widespread but ambiguous concept 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. We discuss model checking of systems controlled by strategies and we present a working strategy-aware model checker built on top of the Maude specification language, based on rewriting logic, and its strategy language.
Title:
Sequence Types for Hereditary Permutators (Download paper)
Abstract:
The invertible terms in Scott’s model D_infty are known as the hereditary permutators. Equivalently, they are terms which are invertible up to βη-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, which gives a positive answer to the problem in the coinductive case.
Title:
Guarded Recursion in Agda via Sized Types (Download paper)
Abstract:
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 commonly 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.
Title:
Cubical Syntax for Reflection-Free Extensional Equality (Download paper)
Abstract:
We contribute XTT, a cubical reconstruction of Observational Type Theory which extends Martin-Lof’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: every closed element of boolean type is derivably equal to either ‘true’ or ‘false’.
Title:
Typed Equivalence of Effect Handlers and Delimited Control (Download paper)
Abstract:
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 shift0 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 interesting type system feature for delimited control operators. Moreover, we extend these results to substantiate the folklore connection between shallow handlers and control flavour of delimited control, both in an untyped and typed settings. All of the results in this paper are formalised in the Coq theorem prover.
Title:
Pointers in Recursion: Exploring the Tropics (Download paper)
Abstract:
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.
Title:
The Delta-calculus: Syntax and Types (Download papers)
Abstract:
We present the ∆-calculus, an explicitly typed λ-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-Salle’, the Coppo-Dezani-Venneri and the Barendregt-Coppo-Dezani ones, producing a family of ∆-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 a la Curry and the corresponding intersection typed systems a la Church by means of an essence function translating an explicitly typed ∆-term into a pure λ-term one. We finally translate a ∆-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 ∆-calculus can be parametrized to take into account other intersection type theories as the ones in the Barendregt et al. book.
Title:
Hilbert’s Tenth Problem in Coq (Download paper)
Abstract:
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 John Conway’s FRACTRAN language as intermediate layer.
Title:
The Discriminating Power of the Let-in Operator1in the Lazy Call-by-Name Probabilistic lambda-Calculus (Download paper)
Abstract:
We consider the notion of probabilistic applicative bismilarity (PAB), recently introduced as a behavioural equivalence over a probabilistic extension of the untyped λ-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 recovering 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.
Title:
Gluing for type theory (Download paper)
Abstract:
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.
Title:
A Lower Bound of the Number of Rewrite Rules Obtained by Homological Methods (Download paper)
Abstract:
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.
Title:
The Sub-Additives: A Proof Theory for Probabilistic Choice extending Linear Logic (Download paper)
Abstract:
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 this logic is a cut elimination result, employing a technique called decomposition.
The justification from the perspective of modelling processes is that implication is sound with respect to established notions of probabilistic refinement, and is fully compositional.
Title:
Proof nets for first-order additive linear logic (Download paper)
Abstract:
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.
Title:
Sparse Tiling through Overlap Closures for Termination of String Rewriting (Download paper)
Abstract:
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 sparse sets of tiles, containing only those that are reachable in derivations. We use the partial algebra defined by a tiling for semantic labeling, to 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.
Title:
A Linear-logical Reconstruction of Intuitionistic Modal Logic S4 (Download papers)
Abstract:
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 gives a sound translation from IS4. Through the Curry–Howard correspondence we further obtain a Geometry of Interaction Machine semantics of the modal λ-calculus by Pfenning and Davies for staged computation.
Title:
Probabilistic Rewriting: Normalization, Termination, and Unique Normal Forms (Download papers)
Abstract:
The motivation behind this work is the need for theoretical tools to support the study of operational properties in probabilistic computation. Indeed, while a mature body of work supports the study of rewriting systems, even infinitary ones, abstract tools for Probabilistic Rewriting are still limited. Probabilistic Abstract Rewriting Systems (PARS) [Bournez-Garnier05] is a setting to formalize an abstract theory of probabilistic rewriting. We study in this setting questions such as “is the result unique?”, or “is there a strategy to find a result with greatest probability?” (normalizing strategies). Both properties are computationally important. Specifically, we propose a robust analogue of “unique normal form” (here, greatest limit distribution), and investigate normalization, and normalizing strategies. We show that transferring standard results is non-trivial, and we propose a family of methods which are well suited to PARS. The goal is to have tools to analyze the operational properties of calculi whose evaluation is both probabilistic and non-deterministic (in the sense that different reductions are possible) such as probabilistic lambda-calculi.
Title:
Modal embeddings and calling paradigms (Download papers)
Abstract:
We study the computational interpretation of the two standard modal embeddings, usually named after Girard and Goedel, 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 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; and that Girard (resp. G”odel) embedding is a translation of cbn (resp. cbv) lambda-calculus into this calculus, enjoying the preservation and reflection properties known for cps translations, but in a stronger form. In particular, the modal target provides a unification of cbn and cbv at the levels of reduction, standard reduction and evaluation. The literature alerts us to the connection between modal embeddings and calling paradigms, but the extent and quality of the connection shown here is a surprise. Additionally, we can translate the modal target itself by “instantiation” of the indeterminate comonad of the comonadic calculus. By composing suitable instantiations with the modal embeddings, we obtain decompositions and improvements of known interpretations of the cbn or cbv lambda-calculus, and show that the explanation of the calling paradigms is entirely given already by the very simple modal target and the embeddings into it.
Title:
Differentials and distances in probabilistic coherence spaces (Download papers)
Abstract:
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. In the first application we show how derivatives allow to compute the expectation of execution time in the weak head reduction of probabilistic PCF (pPCF). In the second one, we apply a general notion of “local” differential of morphisms to the proof of a Lipschitz property of these morhisms 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 Ehrhard-Regnier’s differential lambda-calculus, could be quite meaningful.
Title:
Template games, simple games, and Day convolution (Download paper)
Abstract:
Template games 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, 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. Another instance is Day’s convolution monoidal structure on the category of presheaves over a strict monoidal category, which answers a question raised in the first author’s PhD thesis.
Title:
lambda!-calculus, Intersection Types, and Involutions (Download paper)
Abstract:
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 !_i-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.
Title:
Proof Normalisation in a Logic Identifying Isomorphic Propositions (Download paper)
Abstract:
We define a fragment of propositional logic where isomorphic propositions, such as A&B and B&A, or A=>(B&C) and (A=>B)&(A=>C) are identified. We define System I, a proof language for this logic, and prove its normalisation and consistency.
Title:
On the Taylor Expansion of Probabilistic lambda-terms (Download paper)
Abstract:
We generalize Ehrhard and Regnier’s Taylor Expansion from pure lambda-terms to probabilistic lambda terms through notions of probabilistic resource term and explicit Taylor’s expansion. 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 tight correspondence with Probabilistic Bohm Trees, as introduced by the second author.
Title:
Polymorphic Higher-order Termination (Download paper)
Abstract:
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.
Title:
Homotopy canonicity for cubical type theory (Download paper)
Abstract:
We prove homotopy canonicity for a cubical type theory where the filling operations do not come with computation rules.
Title:
A generic framework for higher-order generalizations (Download paper)
Abstract:
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.
Title:
Dependency Pairs Termination in Dependent Type Theory Modulo Rewriting (Download paper)
Abstract:
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 improves 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 has been implemented in the type-checker Dedukti.
Title:
Deriving an Abstract Machine for Strong Call by Need (Download paper)
Abstract:
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, ie, 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.
Title:
Towards the average-case analysis of substitution resolution in lambda-calculus (Download paper)
Abstract:
Substitution resolution supports the computational character of β-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 β-reduction into an atomic rewriting rule, despite its varying operational complexity. We propose a somewhat indirect average-case analysis of substitution resolution in the classic λ-calculus, based on the quantitative analysis of substitution in λυ, an extension of λ-calculus internalising the υ-calculus of explicit substitutions. Within this framework, we show that for any fixed n≥0, the probability that a uniformly random, conditioned on size, λυ-term υ-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 (Gn)n of regular tree grammars partitioning υ-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 Gn+1 out of Gn 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 λυ-calculus and combinatory logic.
Title:
Modular specification of monads through higher-order presentations (Download paper)
Abstract:
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, and this 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 (Σ,E) of a binding signature Σ and a family E of equations for Σ. This notion of 2-signature has been introduced earlier by Ahrens in a slightly different context.
We associate, to each 2-signature (Σ,E), a category of `models of (Σ,E); and we say that a 2-signature is `effective’ if the associated category of models 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.
Title:
Bicategories in Univalent Foundations (Download paper)
Abstract:
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.
Title:
Probabilistic Programming (Download paper)
Abstract:
Probabilistic programming refers to the idea of developing a programming language for writing and reasoning about probabilistic models from machine learning and statistics. Such a language comes with the implementation of several generic inference algorithms that answer various queries about the models written in the language, such as posterior inference and marginalisation. By providing these algorithms, a probabilistic programming language enables data scientists to focus on designing good models based on their domain knowledge, instead of building effective inference engines for their models, a task that typically requires expertise in machine learning, statistics and systems. Even experts in machine learning and statistics may get benefited from such a probabilistic programming system because using the system they can easily explore highly advanced models.
In the past four years, with colleagues from programming languages, machine learning and probability theory, I have worked on developing the semantic foundations, efficient inference algorithms, and static program analysis for such probabilistic programming languages, especially those that support expressive language features such as higher-order functions, continuous distributions and general recursion. In this talk, I will describe what I have learnt so far.
Sarah Winkler
Title:
Maximal Termination, More Proofs?
Equational Theorem Proving as an Optimization Problem (Download paper)
Abstract:
Maximal completion is a simple yet highly effective approach to classical Knuth-Bendix completion based on maximum satisfiability. In this talk we describe how it also gives rise to a competitive equational theorem prover, and investigate the extension to instantiation-based theorem proving. Particular focus is put on the role of termination techniques.
Amy Felty
Title:
A Linear Logical Framework in Hybrid (Download paper)
Abstract:
We present a linear logical framework implemented within the Hybrid system. 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 a linear specification logic, which provides infrastructure for reasoning directly about object languages with linear features. Our current work includes applications of this framework to proving properties of quantum programming languages, meta-theory of low-level abstract machine code, proof theory of focused linear sequent calculi, and modeling biological processes as transition systems and proving properties about them.
Beniamino Accattoli
Title: A Fresh Look at the Lambda Calculus (Download paper)
Abstract: The (untyped) lambda-calculus is an old topic, almost 90 years old. And yet—I’ll try to argue—its study is far from being over. The talk is a bird’s eye view of the questions I have 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 talk aims at inducing a new way of looking at an old topic, focusing on high-level issues and perspectives.