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.

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.

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.

ABSTRACT. In applications of the Coq proof assistant to correctness of nontrivial programs, my collaborators and I have found an unfortunate tradeoff between proof automation and performance of proof search and checking.  That is, we seem to need to do more manual proof-writing (increasing development time) if we want to control time spent in the proof engine (which also usually increases development time, by introducing delays in exploratory proving).

I'll start by giving a few examples of scripted proof automation at work, for correctness of software and hardware, and then I'll turn to what my collaborators and I have learned about workarounds.  Interestingly for FLOPS, we can identify solutions in the styles of either functional programming or logic programming.  In the functional-programming style, we can effectively reimplement parts of Coq's internals in a more specialized way that can be proved once and for all (in the style of proof by reflection).  We demonstrate this style with an extensible term normalizer and rewriter.  In the direction of logic programming, we investigate fundamental bottlenecks in the handling of unification variables by Coq's proof engine, which mostly has not been designed with lengthy automation scripts in mind.