View: session overviewtalk overview

10:00 | Faithful interpretations of LJT and LJQ into polarized logic PRESENTER: Luís Pinto ABSTRACT. LJT and LJQ are well-known focused sequent calculi with a long history in proof theory and a connection with call-by-name and call-by-value computation, respectively. We are revisiting and problematizing a faithful interpretation of LJT into the focused sequent calculus LJP for polarized logic. Faithfulness allows for the inheritance of a solution space representation developed for LJP and the reuse of known results concerning decision problems related to inhabitation in LJP. Moreover, we are describing work in progress on a faithful interpretation of LJQ into LJP. This result was hinted before in the focusing literature, but we are aiming at a full treatment (the proofs for the fragment with implication and disjunction are settled), technically relying on the use of proof terms. The use of proof terms brings the perspective of inhabitation of simple types by the normal forms of a call-by-value language. |

10:20 | Yet another formal theory of probabilities (with an application to random sampling) ABSTRACT. There are already several formalizations of probability theory in the Coq proof assistant with applications to mathematics, information theory, and programming languages. They have been developed independently, do not cover the same ground, and a substantial effort is required to make them inter-operate. In this presentation, we report about an on-going effort in Coq to port and generalize a library about finite probabilities to a more generic formalization of real analysis called MathComp-Analysis. This gives us an opportunity to generalize results about convexity and probability and to enrich the library of probability inequalities. We explain our process of formalization and apply the resulting library to an original formalization of a random sampling theorem. |

14:00 | Type-Based Termination Checking in Agda ABSTRACT. We present a description of a type-based termination checker for the dependently-typed language Agda. The checker is based on the theory of sized types, i.e., types indexed by an abstract well-ordered type of sizes. It uses a variant of strongly-normalizing higher-order polymorphic lambda calculus with pattern and copattern matching as the semantical foundation. The checker is implemented for Agda, where it is used to certify termination of recursive functions and productivity of corecursive functions. |

14:20 | Size-preserving dependent elimination ABSTRACT. In 2013, the guard condition used in Coq for checking well-foundedness of fixpoints over inductive types was proven incompatible with propositional extensionality. To preserve the compatibility with propositional extensionality, the guard algorithm was restricted but this excluded at the same time some interesting well-foundedness fixpoints such as those obtained by compiling dependent pattern-matching using "small inversion". We propose a less restrictive guard condition that is satisfactory for supporting small-inversion-based compilation of dependent pattern-matching while still being conjectured as compatible with propositional extensionality. We also conjecture this new kind of restriction to support a form of reduction rules for proof-irrelevant propositional equality that does break strong normalisation in the presence of an impredicate universe. |

14:40 | How much do System T recursors lift to dependent types? ABSTRACT. We investigate how to give a foundational role to as-variables in pattern-matching. |

15:00 | A generic translation from case trees to eliminators PRESENTER: Kayleigh Lieverse ABSTRACT. Dependently-typed languages allow one to guarantee correctness of a program by providing formal proofs. The type checkers of such languages elaborate the user-friendly high-level surface language to a small and fully explicit core language. A lot of trust is put into this elaboration process, even though it is rarely verified. One such elaboration is elaborating dependent pattern-matching to the low-level construction of eliminators. This elaboration is done in two steps. First, the function defined by dependent pattern-matching is translated into a case tree, which can then be further translated to eliminators. We present a generic, correct-by-construction translation of this second step in Agda, without the use of metaprogramming and unsafe transformations, by giving a type-safe, correct-by construction, generic definition of case trees and an evaluation function that, given an instantiation of such a case tree and an instantiation of the telescope of function arguments, evaluates the output term of the function using only eliminators. |