Typing Weak MSOL Properties
| Autor: | Igor Walukiewicz, Sylvain Salvati |
|---|---|
| Přispěvatelé: | Laboratoire Bordelais de Recherche en Informatique (LaBRI), Université de Bordeaux (UB)-Centre National de la Recherche Scientifique (CNRS)-École Nationale Supérieure d'Électronique, Informatique et Radiocommunications de Bordeaux (ENSEIRB), Models for a Structured Programming of Space and Time (PoSET), Inria Bordeaux - Sud-Ouest, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Studio de Création et de Recherche en Informatique et Musique Électroacoustique (SCRIME), Université Sciences et Technologies - Bordeaux 1-Université Sciences et Technologies - Bordeaux 1-Laboratoire Bordelais de Recherche en Informatique (LaBRI), Université de Bordeaux (UB)-Centre National de la Recherche Scientifique (CNRS)-École Nationale Supérieure d'Électronique, Informatique et Radiocommunications de Bordeaux (ENSEIRB)-Université de Bordeaux (UB)-Centre National de la Recherche Scientifique (CNRS)-École Nationale Supérieure d'Électronique, Informatique et Radiocommunications de Bordeaux (ENSEIRB), Walukiewicz, Igor, Université de Bordeaux (UB)-École Nationale Supérieure d'Électronique, Informatique et Radiocommunications de Bordeaux (ENSEIRB)-Centre National de la Recherche Scientifique (CNRS)-Université de Bordeaux (UB)-École Nationale Supérieure d'Électronique, Informatique et Radiocommunications de Bordeaux (ENSEIRB)-Centre National de la Recherche Scientifique (CNRS)-Studio de Création et de Recherche en Informatique et Musique Électroacoustique (SCRIME), Université Sciences et Technologies - Bordeaux 1 (UB)-Université Sciences et Technologies - Bordeaux 1 (UB)-Inria Bordeaux - Sud-Ouest, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Université de Bordeaux (UB)-École Nationale Supérieure d'Électronique, Informatique et Radiocommunications de Bordeaux (ENSEIRB)-Centre National de la Recherche Scientifique (CNRS) |
| Jazyk: | angličtina |
| Rok vydání: | 2015 |
| Předmět: |
FOS: Computer and information sciences
Computer Science - Logic in Computer Science [INFO.INFO-LO] Computer Science [cs]/Logic in Computer Science [cs.LO] higher-order verification 0102 computer and information sciences 02 engineering and technology computer.software_genre 01 natural sciences Dependent type Curry–Howard correspondence Denotational semantics Computer Science::Logic in Computer Science LambdaY-Calculus 0202 electrical engineering electronic engineering information engineering Tree automaton 0101 mathematics Mathematics Soundness Functional programming Programming language 010102 general mathematics [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO] 020207 software engineering 16. Peace & justice Logic in Computer Science (cs.LO) TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES 010201 computation theory & mathematics Completeness (logic) TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS Computer Science::Programming Languages 020201 artificial intelligence & image processing computer Normalisation by evaluation |
| Zdroj: | FOSSACS FOSSACS, 2015, London, United Kingdom. pp.343-357, ⟨10.1007/978-3-662-46678-0_22⟩ FOSSACS'15 FOSSACS'15, Apr 2015, London, United Kingdom Lecture Notes in Computer Science ISBN: 9783662466773 FoSSaCS |
| ISSN: | 1860-5974 |
| DOI: | 10.1007/978-3-662-46678-0_22⟩ |
| Popis: | We consider lambda-Y-calculus as a non-interpreted functional programming language: the result of the execution of a program is its normal form that can be seen as the tree of calls to built-in operations. Weak monadic second-order logic (wMSOL) is well suited to express properties of such trees. We give a type system for ensuring that the result of the execution of a lambda-Y-program satisfies a given wMSOL property. In order to prove soundness and completeness of the system we construct a denotational semantics of lambda-Y-calculus that is capable of computing properties expressed in wMSOL. Logical Methods in Computer Science ; Volume 13, Issue 1 ; 1860-5974 |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|