Consuming and Persistent Types for Classical Logic
| Autor: | Delia Kesner, Pierre Vial |
|---|---|
| Rok vydání: | 2020 |
| Předmět: |
Reduction strategy
Natural deduction Theoretical computer science Backtracking Computer science Intersection (set theory) 010102 general mathematics Classical logic Union type Lambda-mu calculus 0102 computer and information sciences Mathematical proof 01 natural sciences 010201 computation theory & mathematics 0101 mathematics |
| Zdroj: | LICS |
| DOI: | 10.1145/3373718.3394774 |
| Popis: | We prove that type systems are able to capture exact measures related to dynamic properties of functional programs with control operators, which allow implementing intricate continuations and backtracking. Our type systems give the number of evaluation steps to normal form as well as the size of this normal form without any evaluation being needed. We focus on Parigot's λμ-calculus, a computational interpretation of classical natural deduction, and our type systems are based upon non-idempotent intersection and union types. We introduce two kinds of arrows: consuming ones, which type function applications that are evaluated/destroyed during reduction, and persistent ones, which type those that are never consumed. These two forms of arrows are the essential tool of our typing systems to deal with control operators, as we are going to show. The main contribution of this paper is a type framework capturing exact measures within the λμ-calculus for 3 different evaluation strategies, namely, head, leftmost-outermost and maximal, associated to the well-known notions of head, weak and strong normalization respectively. Moreover, this is done in a parametric way: we do not provide one type system for each reduction strategy, as it is usually done in the literature, but we give a unique typing system parametrizing key concepts and factorizing common proofs. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|