Practical Subtyping for System F with Sized (Co-)Induction
| Autor: | Lepigre, Rodolphe, Raffalli, Christophe |
|---|---|
| Přispěvatelé: | Laboratoire de Mathématiques (LAMA), Centre National de la Recherche Scientifique (CNRS)-Université Savoie Mont Blanc (USMB [Université de Savoie] [Université de Chambéry]) |
| Jazyk: | angličtina |
| Rok vydání: | 2017 |
| Předmět: |
FOS: Computer and information sciences
Hilbert's epsilon ACM: D.: Software/D.3: PROGRAMMING LANGUAGES/D.3.1: Formal Definitions and Theory/D.3.1.0: Semantics ACM: D.: Software/D.3: PROGRAMMING LANGUAGES/D.3.1: Formal Definitions and Theory/D.3.1.1: Syntax Computer Science - Logic in Computer Science Computer Science - Programming Languages ACM: D.: Software/D.3: PROGRAMMING LANGUAGES/D.3.3: Language Constructs and Features/D.3.3.6: Data types and structures [INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL] subtyping induction and coinduction [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO] ACM: D.: Software/D.3: PROGRAMMING LANGUAGES/D.3.2: Language Classifications/D.3.2.0: Applicative (functional) languages Mathematics - Logic System F strong normalization Logic in Computer Science (cs.LO) polymorphism realizability TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES ACM: D.: Software/D.3: PROGRAMMING LANGUAGES/D.3.3: Language Constructs and Features/D.3.3.13: Polymorphism TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS FOS: Mathematics (Co)inductive types Logic (math.LO) Programming Languages (cs.PL) |
| Popis: | We present a rich type system with subtyping for an extension of System F. Our type constructors include sum and product types, universal and existential quantifiers, inductive and coinductive types. The latter two size annotations allowing the preservation of size invariants. For example it is possible to derive the termination of the quicksort by showing that partitioning a list does not increase its size. The system deals with complex programs involving mixed induction and coinduction, or even mixed (co-)induction and polymorphism (as for Scott-encoded datatypes). One of the key ideas is to completely separate the induction on sizes from the notion of recursive programs. We use the size change principle to check that the proof is well-founded, not that the program terminates. Termination is obtained by a strong normalization proof. Another key idea is the use symbolic witnesses to handle quantifiers of all sorts. To demonstrate the practicality of our system, we provide an implementation that accepts all the examples discussed in the paper and much more. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|