The date for the annunal meeting WG 1.6 is Wednesday, June 26, 2019. The WG 1.6 is part of FSCD and will take place mid-conference.
Abstract:The area of implicit complexity aims to study complexity classes (such as P, NP, LOGSPACE, ...) by encoding queries into calculi or logics. One such approach, introduced by Jones in 2001, is to use read-only ("cons-free") functional programs with restrictions on type orders. In this talk, I describe this work, and discuss the (significant!) effects of using term rewriting systems instead of functional programs.
Abstract:Matrix interpretations are widely used in automated complexity analysis. Certifying such analyses boils down to determining the growth rate of A^n for a fixed non-negative rational matrix A. A direct solution for this task involves the computation of all eigenvalues of A, which often leads to expensive algebraic number computations. We present a new variant of the Perron-Frobenius theorem in order to completely avoid algebraic numbers computations that have previously been necessary when certifying complexity proofs. To formalize the theorem in Isabelle/HOL, we establish a connection between two different Isabelle/HOL libraries on matrices, enabling an easy exchange of theorems between both libraries.
Abstract: The notion of subtyping has gained an important role in lambda and concurrent calculi as well as in programming languages. The soundness and the completeness, together referred to as the preciseness of subtyping, can be considered from two different aspects: denotational and operational. The former preciseness is based on the denotation of a type which is a mathematical object that describes the meaning of the type in accordance with the denotations of other expressions from the language. The latter preciseness has been recently developed for iso-recursive types with respect to type safety, i.e. the safe replacement of a term of a smaller type when a term of a bigger type is expected. We present a technique for formalising and proving operational preciseness of the subtyping relation in concurrent lambda calculus with intersection and union types. An overview of preciseness of subtyping in the setting of session and multiparty session type will be given. We then discuss a universal (language independent) framework to reason about preciseness of subtyping. (The talk is based on the results obtained jointly with Mariangiola Dezani-Ciancaglini, Svetlana Jaksic, Jovanka Pantovic, Alceste Scalas and Nobuko Yoshida.)
- 8:30-9:00 welcome/coffee break
9:00 - 10:00 - session 1
- 09:00-10:00 Cynthia Kop
Cons-Free Rewriting
10:00 - 10:30 - coffee break
10:30 - 13:00 - session 2
- 10:30-11:30 Rene Thiemann
Improved Certification of Complexity Proofs for Term Rewrite Systems
- 11:30-11:45 Herman Geuvers
Informal Report on FSCD
- 11:45-12:30 Report on IFIP (Martin Avanzini)
12:30 - 14:00 - lunch
14:00 - 15:30 - session
- 14:00-15:00 Silvia Ghilezan
Denotational and Operational Preciseness of Subtyping
- 15:00-15:30 Report ISR (Hans Zantema)
- 15:30 - 16:00 - coffee break
- 16:00-17:30 Business Meeting
The meetings of the working group are public, with the single exception of the business meeting.