View: session overviewtalk overview
20:00 | On restriction of cut in cyclic proof system for symbolic heaps PRESENTER: Kenji Saotome ABSTRACT. It has been shown that some variants of cyclic proof systems for symbolic heap entailments in separation logic do not enjoy cut elimination property. In bottom-up proof search, we have to consider the cut rule, which requires some heuristics to find cut formulas. Hence, it is expected to achieve some restricted variant of cut rule which does not change provability and does not interfere automatic proof search without heuristics. This paper gives a strict limit on this challenge. We propose a restricted cut rule, called the presumable cut, in which cut formula is restricted to those which may occur below the cut. This paper shows that there is an entailment which is provable with full cuts, but not with only presumable cuts. |
20:30 | Polynomial time over the reals with parsimony PRESENTER: Romain Péchoux ABSTRACT. We provide a characterization of Ko's class of polynomial time computable functions over real numbers. This characterization holds for a stream based language using a parsimonious type discipline, a variant of propositional linear logic. We obtain a first characterization of polynomial time computations over the reals on a higher-order functional language using a linear/affine type system. |
21:00 | Session Types without Sophistry (System Description) PRESENTER: Keigo Imai ABSTRACT. Whereas ordinary types approximate the results, session types approximate communication among computations. As a form of typestate, they describe not only what is communicated now but also what is to be communicated next. Writing session-typed programs in an ordinary programming language such an OCaml requires inordinary cleverness to simulate type-level computations and linear typing~-- meaning the implementation and the error messages are very hard to understand. One is constantly reminded of template metaprogramming in C++. We present a system exploring a very different approach to session typing: lowering type-level sophistry to ordinary programming, while maintaining the static assurances. Error messages are detailed and customizable, and one can use an ordinary debugger to investigate session-type problems. Our system is a binary-session--typed DSL for service-oriented programming in OCaml, supporting multiple communication channels, internal and external choices, and also channel delegation. The key idea is staging: ordinary run-time checks in the generator play the role of `type-checks' from the point of view of the generated program. What is a fancy type to the latter is ordinary data to the generator. |