Descriptor: "[ INFO.INFO-PL ] Computer Science [cs]/Programming Languages [cs.PL]" / Topic: 0202 electrical engineering, electronic engineering, information engineering - Searchworks@Jio Institute Digital Library Search Results

Your search keyword '"[ INFO.INFO-PL ] Computer Science [cs]/Programming Languages [cs.PL]"' showing total 17 results

Start Over Descriptor "[ INFO.INFO-PL ] Computer Science [cs]/Programming Languages [cs.PL]" Topic 0202 electrical engineering, electronic engineering, information engineering

17 results on '"[ INFO.INFO-PL ] Computer Science [cs]/Programming Languages [cs.PL]"'

1. Towards Certified Meta-Programming with Typed Template-Coq

Author: Nicolas Tabareau, Abhishek Anand, Cyril Cohen, Matthieu Sozeau, Simon Boulier, Cornell University [New York], Gallinette : vers une nouvelle génération d'assistant à la preuve (GALLINETTE), Inria Rennes – Bretagne Atlantique, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire des Sciences du Numérique de Nantes (LS2N), IMT Atlantique Bretagne-Pays de la Loire (IMT Atlantique), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT)-Université de Nantes - UFR des Sciences et des Techniques (UN UFR ST), Université de Nantes (UN)-Université de Nantes (UN)-École Centrale de Nantes (ECN)-Centre National de la Recherche Scientifique (CNRS)-IMT Atlantique Bretagne-Pays de la Loire (IMT Atlantique), Université de Nantes (UN)-Université de Nantes (UN)-École Centrale de Nantes (ECN)-Centre National de la Recherche Scientifique (CNRS), Mathematical, Reasoning and Software (MARELLE), Inria Sophia Antipolis - Méditerranée (CRISAM), Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Design, study and implementation of languages for proofs and programs (PI.R2), Université Paris Diderot - Paris 7 (UPD7)-Centre National de la Recherche Scientifique (CNRS)-Institut de Recherche en Informatique Fondamentale (IRIF (UMR_8243)), Université Paris Diderot - Paris 7 (UPD7)-Centre National de la Recherche Scientifique (CNRS)-Université Paris Diderot - Paris 7 (UPD7)-Centre National de la Recherche Scientifique (CNRS)-Inria de Paris, Département Automatique, Productique et Informatique (IMT Atlantique - DAPI), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT), This work is supported by the CoqHoTT ERC Grant 64399 and the NSF grants CCF-1407794, CCF-1521602, and CCF-1646417., European Project: 637339,H2020 ERC,ERC-2014-STG,CoqHoTT(2015), Cornell University, GALLINETTE ( GALLINETTE ), Laboratoire des Sciences du Numérique de Nantes ( LS2N ), Université de Nantes ( UN ) -École Centrale de Nantes ( ECN ) -Centre National de la Recherche Scientifique ( CNRS ) -IMT Atlantique Bretagne-Pays de la Loire ( IMT Atlantique ) -Université de Nantes ( UN ) -École Centrale de Nantes ( ECN ) -Centre National de la Recherche Scientifique ( CNRS ) -IMT Atlantique Bretagne-Pays de la Loire ( IMT Atlantique ) -Inria Rennes – Bretagne Atlantique, Institut National de Recherche en Informatique et en Automatique ( Inria ) -Institut National de Recherche en Informatique et en Automatique ( Inria ), Mathematical, Reasoning and Software ( MARELLE ), Inria Sophia Antipolis - Méditerranée ( CRISAM ), Design, study and implementation of languages for proofs and programs ( PI.R2 ), Preuves, Programmes et Systèmes ( PPS ), Université Paris Diderot - Paris 7 ( UPD7 ) -Centre National de la Recherche Scientifique ( CNRS ) -Université Paris Diderot - Paris 7 ( UPD7 ) -Centre National de la Recherche Scientifique ( CNRS ) -Centre National de la Recherche Scientifique ( CNRS ) -Inria de Paris, European Project : 637339,H2020 ERC,ERC-2014-STG,CoqHoTT ( 2015 ), Gallinette : vers une nouvelle génération d'assistant à la preuve (LS2N - équipe GALLINETTE), Université de Nantes - UFR des Sciences et des Techniques (UN UFR ST), Université de Nantes (UN)-Université de Nantes (UN)-École Centrale de Nantes (ECN)-Centre National de la Recherche Scientifique (CNRS)-IMT Atlantique (IMT Atlantique), IMT Atlantique (IMT Atlantique), Université de Nantes - Faculté des Sciences et des Techniques, and Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT)-Université de Nantes - Faculté des Sciences et des Techniques
Subjects: Correctness, [INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL], Syntax (programming languages), Semantics (computer science), Computer science, Programming language, 020207 software engineering, 02 engineering and technology, computer.software_genre, Metaprogramming, Operational semantics, Type theory, TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, Formal specification, [ INFO.INFO-PL ] Computer Science [cs]/Programming Languages [cs.PL], TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, 0202 electrical engineering, electronic engineering, information engineering, 020201 artificial intelligence & image processing, Parametricity, computer
Abstract: International audience; Template-Coq is a plugin for Coq, originally implemented by Malecha, which provides a reifier for Coq terms and global declarations , as represented in the Coq kernel, as well as a denotation command. Initially, it was developed for the purpose of writing functions on Coq's AST in Gallina. Recently, it was used in the CertiCoq certified compiler project, as its front-end language, to derive parametricity properties, and to extract Coq terms to a CBV λ-calculus. However, the syntax lacked semantics, be it typing semantics or operational semantics, which should reflect, as formal specifications in Coq, the semantics of Coq's type theory itself. The tool was also rather bare bones, providing only rudimentary quoting and unquoting commands. We generalize it to handle the entire Calculus of Inductive Constructions (CIC), as implemented by Coq, including the kernel's declaration structures for definitions and inductives, and implement a monad for general manipulation of Coq's logical environment. We demonstrate how this setup allows Coq users to define many kinds of general purpose plugins, whose correctness can be readily proved in the system itself, and that can be run efficiently after extraction. We give a few examples of implemented plugins, including a parametricity translation. We also advocate the use of Template-Coq as a foundation for higher-level tools.
Published: 2018
Full Text: View/download PDF

2. Extending Timbuk to Verify Functional Programs

Author: Timothée Haudebourg, Sébastien Lê Cong, Tristan Gillard, Thomas Genet, Software certification with semantic analysis ( CELTIQUE ), Inria Rennes – Bretagne Atlantique, Institut National de Recherche en Informatique et en Automatique ( Inria ) -Institut National de Recherche en Informatique et en Automatique ( Inria ) -LANGAGE ET GÉNIE LOGICIEL ( IRISA_D4 ), Institut de Recherche en Informatique et Systèmes Aléatoires ( IRISA ), Université de Rennes 1 ( UR1 ), Université de Rennes ( UNIV-RENNES ) -Université de Rennes ( UNIV-RENNES ) -Institut National des Sciences Appliquées - Rennes ( INSA Rennes ) -Université de Bretagne Sud ( UBS ) -École normale supérieure - Rennes ( ENS Rennes ) -Institut National de Recherche en Informatique et en Automatique ( Inria ) -CentraleSupélec-Centre National de la Recherche Scientifique ( CNRS ) -IMT Atlantique Bretagne-Pays de la Loire ( IMT Atlantique ) -Université de Rennes 1 ( UR1 ), Université de Rennes ( UNIV-RENNES ) -Université de Rennes ( UNIV-RENNES ) -Institut National des Sciences Appliquées - Rennes ( INSA Rennes ) -Université de Bretagne Sud ( UBS ) -École normale supérieure - Rennes ( ENS Rennes ) -Institut National de Recherche en Informatique et en Automatique ( Inria ) -CentraleSupélec-Centre National de la Recherche Scientifique ( CNRS ) -IMT Atlantique Bretagne-Pays de la Loire ( IMT Atlantique ) -Institut de Recherche en Informatique et Systèmes Aléatoires ( IRISA ), Université de Rennes ( UNIV-RENNES ) -Université de Rennes ( UNIV-RENNES ) -Institut National des Sciences Appliquées - Rennes ( INSA Rennes ) -Université de Bretagne Sud ( UBS ) -École normale supérieure - Rennes ( ENS Rennes ) -CentraleSupélec-Centre National de la Recherche Scientifique ( CNRS ) -IMT Atlantique Bretagne-Pays de la Loire ( IMT Atlantique ), Software certification with semantic analysis (CELTIQUE), Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-LANGAGE ET GÉNIE LOGICIEL (IRISA-D4), Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA), Université de Rennes 1 (UR1), Université de Rennes (UNIV-RENNES)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-IMT Atlantique Bretagne-Pays de la Loire (IMT Atlantique), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT)-Université de Rennes 1 (UR1), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT)-Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA), Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-IMT Atlantique Bretagne-Pays de la Loire (IMT Atlantique), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT), Bio-Inspired, Situated and Cellular Unconventional Information Technologies (BISCUIT), Department of Complex Systems, Artificial Intelligence & Robotics (LORIA - AIS), Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), Logic and Applications (LogicA), LANGAGE ET GÉNIE LOGICIEL (IRISA-D4), CentraleSupélec-Télécom Bretagne-Université de Rennes 1 (UR1), Université de Rennes (UNIV-RENNES)-Université de Rennes (UNIV-RENNES)-Institut National de Recherche en Informatique et en Automatique (Inria)-École normale supérieure - Rennes (ENS Rennes)-Université de Bretagne Sud (UBS)-Centre National de la Recherche Scientifique (CNRS)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-CentraleSupélec-Télécom Bretagne-Université de Rennes 1 (UR1), Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA), Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-École normale supérieure - Cachan (ENS Cachan), Université de Rennes (UR)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-IMT Atlantique (IMT Atlantique), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT)-Université de Rennes (UR)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-IMT Atlantique (IMT Atlantique), École normale supérieure - Cachan (ENS Cachan)-Université de Rennes (UR)-LANGAGE ET GÉNIE LOGICIEL (IRISA-D4), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Institut National de Recherche en Informatique et en Automatique (Inria)-Télécom Bretagne-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-Université de Rennes (UR)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Institut National de Recherche en Informatique et en Automatique (Inria)-Télécom Bretagne-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Institut National de Recherche en Informatique et en Automatique (Inria)-Télécom Bretagne-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Institut National de Recherche en Informatique et en Automatique (Inria)-Télécom Bretagne-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS), Université de Bretagne Sud (UBS)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National de Recherche en Informatique et en Automatique (Inria)-École normale supérieure - Rennes (ENS Rennes)-Centre National de la Recherche Scientifique (CNRS)-Université de Rennes 1 (UR1), Université de Rennes (UNIV-RENNES)-CentraleSupélec-IMT Atlantique Bretagne-Pays de la Loire (IMT Atlantique), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT)-Université de Bretagne Sud (UBS)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-École normale supérieure - Rennes (ENS Rennes)-Centre National de la Recherche Scientifique (CNRS)-Université de Rennes 1 (UR1), Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria), École normale supérieure - Cachan (ENS Cachan)-Université de Rennes 1 (UR1), Université de Rennes (UNIV-RENNES)-Université de Rennes (UNIV-RENNES)-LANGAGE ET GÉNIE LOGICIEL (IRISA-D4), Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-CentraleSupélec-Télécom Bretagne-Institut National de Recherche en Informatique et en Automatique (Inria)-École normale supérieure - Rennes (ENS Rennes)-Université de Bretagne Sud (UBS)-Centre National de la Recherche Scientifique (CNRS)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), and Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)
Subjects: [INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL], Theoretical computer science, Property (programming), Computer science, Parameterized complexity, [INFO.INFO-SE]Computer Science [cs]/Software Engineering [cs.SE], 0102 computer and information sciences, 02 engineering and technology, Extension (predicate logic), [ INFO.INFO-SE ] Computer Science [cs]/Software Engineering [cs.SE], Term (logic), 01 natural sciences, Automaton, Set (abstract data type), Tree (data structure), [INFO.INFO-FL]Computer Science [cs]/Formal Languages and Automata Theory [cs.FL], 010201 computation theory & mathematics, [ INFO.INFO-FL ] Computer Science [cs]/Formal Languages and Automata Theory [cs.FL], [ INFO.INFO-PL ] Computer Science [cs]/Programming Languages [cs.PL], 0202 electrical engineering, electronic engineering, information engineering, 020201 artificial intelligence & image processing, Rewriting system
Abstract: International audience; Timbuk implements the Tree Automata Completion algorithm whose purpose is to over-approximate sets of terms reachable by a term rewriting system. Completion is parameterized by a set of equations defining which terms are equated in the approximation. In this paper we present two extensions of Timbuk which permit us to automatically verify safety properties on functional programs. The first extension is a language, based on regular tree expressions, which eases the specification of the property to prove on the program. The second extension automatically generates a set of equations adapted to the property to prove on the program.
Published: 2018
Full Text: View/download PDF

3. Implementing Modular Class-based Reuse Mechanisms on Top of a Single Inheritance VM

Author: Noury Bouraqadi, Pablo Tesone, Guillermo Polito, Stéphane Ducasse, Luc Fabresse, Centre for Digital Systems (CERI SN), Ecole nationale supérieure Mines-Télécom Lille Douai (IMT Lille Douai), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT), Analyses and Languages Constructs for Object-Oriented Application Evolution (RMOD), Inria Lille - Nord Europe, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre de Recherche en Informatique, Signal et Automatique de Lille - UMR 9189 (CRIStAL), Centrale Lille-Université de Lille-Centre National de la Recherche Scientifique (CNRS)-Centrale Lille-Université de Lille-Centre National de la Recherche Scientifique (CNRS), Centre de Recherche en Informatique, Signal et Automatique de Lille - UMR 9189 (CRIStAL), Centrale Lille-Université de Lille-Centre National de la Recherche Scientifique (CNRS), ACM/SIGAPP, Centre for Digital Systems (CERI SN - IMT Nord Europe), Ecole nationale supérieure Mines-Télécom Lille Douai (IMT Nord Europe), Unité de Recherche Informatique et Automatique ( URIA ), École des Mines de Douai ( Mines Douai EMD ), Institut Mines-Télécom [Paris]-Institut Mines-Télécom [Paris]-PRES Université Lille Nord de France, Analyses and Languages Constructs for Object-Oriented Application Evolution ( RMOD ), Institut National de Recherche en Informatique et en Automatique ( Inria ) -Institut National de Recherche en Informatique et en Automatique ( Inria ) -Centre de Recherche en Informatique, Signal et Automatique de Lille (CRIStAL) - UMR 9189 ( CRIStAL ), Institut National de Recherche en Informatique et en Automatique ( Inria ) -Ecole Centrale de Lille-Institut Mines-Télécom [Paris]-Université de Lille-Centre National de la Recherche Scientifique ( CNRS ) -Ecole Centrale de Lille-Institut Mines-Télécom [Paris]-Université de Lille-Centre National de la Recherche Scientifique ( CNRS ), Centre de Recherche en Informatique, Signal et Automatique de Lille (CRIStAL) - UMR 9189 ( CRIStAL ), and Institut National de Recherche en Informatique et en Automatique ( Inria ) -Ecole Centrale de Lille-Institut Mines-Télécom [Paris]-Université de Lille-Centre National de la Recherche Scientifique ( CNRS )
Subjects: code reuse, composable language features, [INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL], Computer science, business.industry, Programming language, Multiple inheritance, Code reuse, Software development, 020207 software engineering, 02 engineering and technology, computer.software_genre, 020202 computer hardware & architecture, Inheritance (object-oriented programming), [ INFO.INFO-PL ] Computer Science [cs]/Programming Languages [cs.PL], 0202 electrical engineering, electronic engineering, information engineering, Programming paradigm, business, Protocol (object-oriented programming), Execution model, computer, Implementation, performance
Abstract: International audience; Code reuse is a good strategy to avoid code duplication and speed up software development. Existing object-oriented programming languages propose different ways of combining existing and new code such as e.g., single inheritance, multiple inheritance, Traits or Mixins. All these mechanisms present advantages and disadvantages and there are situations that require the use of one over the other. To avoid the complexity of implementing a virtual machine (VM), many of these mechanisms are often implemented on top of an existing high-performance VM, originally meant to run a single inheritance object-oriented language. These implementations require thus a mapping between the programming model they propose and the execution model provided by the VM. Moreover, reuse mechanisms are not usually composable, nor it is easy to implement new ones for a given language. In this paper, we propose a modular meta-level runtime architecture to implement and combine different code reuse mechanisms. This architecture supports dynamic combination of several mechanisms without affecting runtime performance in a single inheritance object-oriented VM. It includes moreover a reflective Meta-Object Protocol to query and modify classes using the programming logical model instead of the underlying low-level runtime model. Thanks to this architecture, we implemented Stateful Traits, Mixins, CLOS multiple inheritance, CLOS Standard Method Combinations and Beta prefixing in a modular and composable way.
Published: 2018
Full Text: View/download PDF

4. Foundations of Dependent Interoperability

Author: Pierre-Évariste Dagand, Nicolas Tabareau, Éric Tanter, Well Honed Infrastructure Software for Programming Environments and Runtimes ( Whisper ), Laboratoire d'Informatique de Paris 6 ( LIP6 ), Université Pierre et Marie Curie - Paris 6 ( UPMC ) -Centre National de la Recherche Scientifique ( CNRS ) -Université Pierre et Marie Curie - Paris 6 ( UPMC ) -Centre National de la Recherche Scientifique ( CNRS ) -Inria de Paris, Institut National de Recherche en Informatique et en Automatique ( Inria ) -Institut National de Recherche en Informatique et en Automatique ( Inria ), GALLINETTE ( GALLINETTE ), Inria Rennes – Bretagne Atlantique, Institut National de Recherche en Informatique et en Automatique ( Inria ) -Institut National de Recherche en Informatique et en Automatique ( Inria ) -Laboratoire des Sciences du Numérique de Nantes ( LS2N ), Université de Nantes ( UN ) -École Centrale de Nantes ( ECN ) -Centre National de la Recherche Scientifique ( CNRS ) -IMT Atlantique Bretagne-Pays de la Loire ( IMT Atlantique ) -Université de Nantes ( UN ) -École Centrale de Nantes ( ECN ) -Centre National de la Recherche Scientifique ( CNRS ) -IMT Atlantique Bretagne-Pays de la Loire ( IMT Atlantique ), Automatique, productique et informatique ( DAPI ), IMT Atlantique Bretagne-Pays de la Loire ( IMT Atlantique ), Department of Computer Science [Santiago, Chile] ( DCC ), University of Chile [Santiago], European Project : 637339,H2020 ERC,ERC-2014-STG,CoqHoTT ( 2015 ), Well Honed Infrastructure Software for Programming Environments and Runtimes ( Whisper), Inria de Paris, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-LIP6, Sorbonne Université (SU)-Centre National de la Recherche Scientifique (CNRS)-Sorbonne Université (SU)-Centre National de la Recherche Scientifique (CNRS), Gallinette : vers une nouvelle génération d'assistant à la preuve (GALLINETTE), Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire des Sciences du Numérique de Nantes (LS2N), IMT Atlantique Bretagne-Pays de la Loire (IMT Atlantique), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT)-Université de Nantes - UFR des Sciences et des Techniques (UN UFR ST), Université de Nantes (UN)-Université de Nantes (UN)-École Centrale de Nantes (ECN)-Centre National de la Recherche Scientifique (CNRS)-IMT Atlantique Bretagne-Pays de la Loire (IMT Atlantique), Université de Nantes (UN)-Université de Nantes (UN)-École Centrale de Nantes (ECN)-Centre National de la Recherche Scientifique (CNRS), Département Automatique, Productique et Informatique (IMT Atlantique - DAPI), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT), Department of Computer Science [Santiago, Chile] (DCC), Universidad de Chile = University of Chile [Santiago] (UCHILE), European Project: 637339,H2020 ERC,ERC-2014-STG,CoqHoTT(2015), Well Honed Infrastructure Software for Programming Environments and Runtimes (Whisper), Gallinette : vers une nouvelle génération d'assistant à la preuve (LS2N - équipe GALLINETTE), Université de Nantes - UFR des Sciences et des Techniques (UN UFR ST), Université de Nantes (UN)-Université de Nantes (UN)-École Centrale de Nantes (ECN)-Centre National de la Recherche Scientifique (CNRS)-IMT Atlantique (IMT Atlantique), and IMT Atlantique (IMT Atlantique)
Subjects: Theoretical computer science, Computer science, Interoperability, 0102 computer and information sciences, 02 engineering and technology, Galois connection, 01 natural sciences, Constructive, Software, ACM : F.: Theory of Computation/F.4: MATHEMATICAL LOGIC AND FORMAL LANGUAGES/F.4.1: Mathematical Logic/F.4.1.2: Lambda calculus and related systems, [ INFO.INFO-PL ] Computer Science [cs]/Programming Languages [cs.PL], 0202 electrical engineering, electronic engineering, information engineering, Equivalence (formal languages), ACM: F.: Theory of Computation/F.3: LOGICS AND MEANINGS OF PROGRAMS/F.3.3: Studies of Program Constructs/F.3.3.4: Type structure, 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], business.industry, 020207 software engineering, Data structure, ACM: F.: Theory of Computation/F.4: MATHEMATICAL LOGIC AND FORMAL LANGUAGES/F.4.1: Mathematical Logic/F.4.1.2: Lambda calculus and related systems, ACM : D.: Software/D.3: PROGRAMMING LANGUAGES/D.3.3: Language Constructs and Features/D.3.3.6: Data types and structures, Monotone polygon, ACM : F.: Theory of Computation/F.3: LOGICS AND MEANINGS OF PROGRAMS/F.3.3: Studies of Program Constructs/F.3.3.4: Type structure, 010201 computation theory & mathematics, Homotopy type theory, business
Abstract: Full-spectrum dependent types promise to enable the development of correct-by-construction software. However, even certified software needs to interact with simply-typed or untyped programs, be it to perform system calls, or to use legacy libraries. Trading static guarantees for runtime checks, thedependent interoperabilityframework provides a mechanism by which simply-typed values can safely be coerced to dependent types and, conversely, dependently-typed programs can defensively be exported to a simply-typed application. In this article, we give a semantic account of dependent interoperability. Our presentation relies on and is guided by a pervading notion of type equivalence, whose importance has been emphasized in recent work on homotopy type theory. Specifically, we develop the notions oftype-theoretic partial Galois connectionsas a key foundation for dependent interoperability, which accounts for the partiality of the coercions between types. We explore the applicability of both type-theoretic Galois connections and anticonnections in the setting of dependent interoperability. A partial Galois connection enforces a translation of dependent types to runtime checks that are both sound and complete with respect to the invariants encoded by dependent types. Conversely, picking an anticonnection instead lets us induce weaker, sound conditions that can amount to more efficient runtime checks.Our framework is developed in Coq; it is thus constructive and verified in the strictest sense of the terms. Using our library, users can specify domain-specific partial connections between data structures. Our library then takes care of the (sometimes, heavy) lifting that leads to interoperable programs. It thus becomes possible, as we shall illustrate, to internalize and hand-tune the extraction of dependently-typed programs to interoperable OCaml programs within Coq itself.
Published: 2018
Full Text: View/download PDF

5. Scalable Machine Learning for Predicting At-Risk Profiles Upon Hospital Admission

Author: Pierre Genevès, Nabil Layaïda, Jean-Luc Bosson, Svetlana Artemova, Marion Lepelley, Thomas Calmant, Types and Reasoning for the Web (TYREX), Inria Grenoble - Rhône-Alpes, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire d'Informatique de Grenoble (LIG ), Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Centre National de la Recherche Scientifique (CNRS)-Université Grenoble Alpes [2016-2019] (UGA [2016-2019])-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Centre National de la Recherche Scientifique (CNRS)-Université Grenoble Alpes [2016-2019] (UGA [2016-2019]), SED [Grenoble], Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Centre Hospitalier Universitaire [Grenoble] (CHU), ANR-16-CE25-0010,CLEAR,Compilation de langages intermédiaires en exécutables efficaces pour le big data(2016), Service Expérimentation et Développement (SED [Grenoble]), Types and Reasoning for the Web ( TYREX ), Institut National de Recherche en Informatique et en Automatique ( Inria ) -Institut National de Recherche en Informatique et en Automatique ( Inria ) -Laboratoire d'Informatique de Grenoble ( LIG ), Université Pierre Mendès France - Grenoble 2 ( UPMF ) -Université Joseph Fourier - Grenoble 1 ( UJF ) -Institut National Polytechnique de Grenoble ( INPG ) -Centre National de la Recherche Scientifique ( CNRS ) -Université Grenoble Alpes ( UGA ) -Université Pierre Mendès France - Grenoble 2 ( UPMF ) -Université Joseph Fourier - Grenoble 1 ( UJF ) -Institut National Polytechnique de Grenoble ( INPG ) -Centre National de la Recherche Scientifique ( CNRS ) -Université Grenoble Alpes ( UGA ), Centre Hospitalier Universitaire [Grenoble] ( CHU ), and ANR : CLEAR,ANR Project CLEAR (ANR-16-CE25-0010)
Subjects: Information Systems and Management, big prescription data, Computer science, Big data, 02 engineering and technology, Machine learning, computer.software_genre, [ INFO.INFO-LG ] Computer Science [cs]/Machine Learning [cs.LG], Management Information Systems, [INFO.INFO-AI]Computer Science [cs]/Artificial Intelligence [cs.AI], [ INFO.INFO-DC ] Computer Science [cs]/Distributed, Parallel, and Cluster Computing [cs.DC], [INFO.INFO-LG]Computer Science [cs]/Machine Learning [cs.LG], [STAT.ML]Statistics [stat]/Machine Learning [stat.ML], 020204 information systems, [ INFO.INFO-PL ] Computer Science [cs]/Programming Languages [cs.PL], 0202 electrical engineering, electronic engineering, information engineering, [ INFO.INFO-AI ] Computer Science [cs]/Artificial Intelligence [cs.AI], [ STAT.ML ] Statistics [stat]/Machine Learning [stat.ML], volume, [INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL], business.industry, Medical record, Volume (computing), Construct (python library), experiments, Predictive analytics, [SDV.SP]Life Sciences [q-bio]/Pharmaceutical sciences, 3. Good health, Computer Science Applications, Variety (cybernetics), predictive analytics, variety, [ SDV.SP ] Life Sciences [q-bio]/Pharmaceutical sciences, Binary classification, Scalability, 020201 artificial intelligence & image processing, Artificial intelligence, [INFO.INFO-DC]Computer Science [cs]/Distributed, Parallel, and Cluster Computing [cs.DC], business, computer, application, Information Systems
Abstract: International audience; We show how the analysis of very large amounts of drug prescription data make it possible to detect, on the day of hospital admission, patients at risk of developing complications during their hospital stay. We explore, for the first time, to which extent volume and variety of big prescription data help in constructing predictive models for the automatic detection of at-risk profiles.Our methodology is designed to validate our claims that: (1) drug prescription data on the day of admission contain rich information about the patient's situation and perspectives of evolution, and (2) the various perspectives of big medical data (such as veracity, volume, variety) help in extracting this information.We build binary classification models to identify at-risk patient profiles. We use a distributed architecture to ensure scalability of model construction with large volumes of medical records and clinical data. We report on practical experiments with real data of millions of patients and hundreds of hospitals. We demonstrate how the fine-grained analysis of such big data can improve the detection of at-risk patients, making it possible to construct more accurate predictive models that significantly benefit from volume and variety, while satisfying important criteria to be deployed in hospitals.
Published: 2018
Full Text: View/download PDF

6. A polyhedral compilation framework for loops with dynamic data-dependent bounds

Author: Michael Kruse, Jie Zhao, Albert Cohen, Parallélisme de Kahn Synchrone ( Parkas), Département d'informatique - ENS Paris (DI-ENS), École normale supérieure - Paris (ENS-PSL), Université Paris sciences et lettres (PSL)-Université Paris sciences et lettres (PSL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure - Paris (ENS-PSL), Université Paris sciences et lettres (PSL)-Université Paris sciences et lettres (PSL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Centre National de la Recherche Scientifique (CNRS)-Inria de Paris, Institut National de Recherche en Informatique et en Automatique (Inria), Parallélisme de Kahn Synchrone ( Parkas ), Inria de Paris, Institut National de Recherche en Informatique et en Automatique ( Inria ) -Institut National de Recherche en Informatique et en Automatique ( Inria ) -Département d'informatique de l'École normale supérieure ( DI-ENS ), École normale supérieure - Paris ( ENS Paris ) -Institut National de Recherche en Informatique et en Automatique ( Inria ) -Centre National de la Recherche Scientifique ( CNRS ) -École normale supérieure - Paris ( ENS Paris ) -Centre National de la Recherche Scientifique ( CNRS ) -Centre National de la Recherche Scientifique ( CNRS ), Département d'informatique de l'École normale supérieure (DI-ENS), École normale supérieure - Paris (ENS Paris), Université Paris sciences et lettres (PSL)-Université Paris sciences et lettres (PSL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure - Paris (ENS Paris), Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Département d'informatique - ENS Paris (DI-ENS), Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-École normale supérieure - Paris (ENS Paris), Université Paris sciences et lettres (PSL)-Université Paris sciences et lettres (PSL)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure - Paris (ENS Paris), and Université Paris sciences et lettres (PSL)-Université Paris sciences et lettres (PSL)-Centre National de la Recherche Scientifique (CNRS)
Subjects: Computer science, 010103 numerical & computational mathematics, 02 engineering and technology, pilers, 01 natural sciences, Parallelizing compiler, [ INFO.INFO-PL ] Computer Science [cs]/Programming Languages [cs.PL], Loop nest optimization, 0202 electrical engineering, electronic engineering, information engineering, Polytope model, Code generation, 0101 mathematics, [INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL], Dynamic data, 020207 software engineering, Polyhedral model, CCS Concepts • Software and its engineering → Com, Dynamic programming, Compilers, Vectorization (mathematics), Keywords parallelizing compiler, While loop, Dynamic counted loop, Affine transformation, Algorithm
Abstract: International audience; We study the parallelizing compilation and loop nest optimization of an important class of programs where counted loops have a dynamic data-dependent upper bound. Such loops are amenable to a wider set of transformations than general while loops with inductively defined termination conditions: for example, the substitution of closed forms for induction variables remains applicable, removing the loop-carried data dependences induced by termination conditions. We propose an automatic compilation approach to parallelize and optimize dynamic counted loops. Our approach relies on affine relations only, as implemented in state-of-the-art polyhedral libraries. Revisiting a state-of-the-art framework to parallelize arbitrary while loops, we introduce additional control dependences on data-dependent predicates. Our method goes beyond the state of the art in fully automating the process, specializing the code generation algorithm to the case of dynamic counted loops and avoiding the introduction of spurious loop-carried dependences. We conduct experiments on representative irregular computations, from dynamic programming, computer vision and finite element methods to sparse matrix linear algebra. We validate that the method is applicable to general affine transformations for locality optimization, vectorization and parallelization.
Published: 2018
Full Text: View/download PDF

7. A Survey of Parametric Dataflow Models of Computation

Author: Pascal Fradet, Adnan Bouakaz, Alain Girault, Sound Programming of Adaptive Dependable Embedded Systems (SPADES), Inria Grenoble - Rhône-Alpes, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire d'Informatique de Grenoble (LIG ), Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Centre National de la Recherche Scientifique (CNRS)-Université Grenoble Alpes [2016-2019] (UGA [2016-2019])-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Centre National de la Recherche Scientifique (CNRS)-Université Grenoble Alpes [2016-2019] (UGA [2016-2019]), Sound Programming of Adaptive Dependable Embedded Systems ( SPADES ), and Institut National de Recherche en Informatique et en Automatique ( Inria ) -Institut National de Recherche en Informatique et en Automatique ( Inria )
Subjects: Computer science, Dataflow, 02 engineering and technology, Parallel computing, [ INFO.INFO-PL ] Computer Science [cs]/Programming Languages [cs.PL], 0202 electrical engineering, electronic engineering, information engineering, [ INFO.INFO-ES ] Computer Science [cs]/Embedded Systems, Electrical and Electronic Engineering, Dataflow architecture, Parametric statistics, Static analyses, Signal processing, [INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL], Model of computation, Parametrization, Control reconfiguration, 020206 networking & telecommunications, Static analysis, Computer Graphics and Computer-Aided Design, 020202 computer hardware & architecture, Computer Science Applications, Computer engineering, Dataflow models of computation, Reconfiguration, [INFO.INFO-ES]Computer Science [cs]/Embedded Systems
Abstract: Dataflow models of computation (MoCs) are widely used to design embedded signal processing and streaming systems. Dozens of dataflow MoCs have been proposed in the past few decades. More recently, several parametric dataflow MoCs have been presented as an interesting tradeoff between analyzability and expressiveness. They offer a controlled form of dynamism under the form of parameters (e.g., parametric rates), along with runtime parameter configuration. This survey provides a comprehensive description of the existing parametric dataflow MoCs (constructs, constraints, properties, static analyses) and compares them using a common example. The main objectives are to help designers of streaming applications choose the most suitable model for their needs and pave the way for the design of new parametric MoCs.
Published: 2017

8. Symbolic Analyses of Dataflow Graphs

Author: Adnan Bouakaz, Alain Girault, Pascal Fradet, Sound Programming of Adaptive Dependable Embedded Systems ( SPADES ), Inria Grenoble - Rhône-Alpes, Institut National de Recherche en Informatique et en Automatique ( Inria ) -Institut National de Recherche en Informatique et en Automatique ( Inria ), Sound Programming of Adaptive Dependable Embedded Systems (SPADES), Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire d'Informatique de Grenoble (LIG ), and Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Centre National de la Recherche Scientifique (CNRS)-Université Grenoble Alpes [2016-2019] (UGA [2016-2019])-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Centre National de la Recherche Scientifique (CNRS)-Université Grenoble Alpes [2016-2019] (UGA [2016-2019])
Subjects: ACM: F.: Theory of Computation/F.1: COMPUTATION BY ABSTRACT DEVICES/F.1.1: Models of Computation, Computer science, Dataflow, Design space exploration, Dataflow graphs, 02 engineering and technology, Parallel computing, 01 natural sciences, Symbolic data analysis, Scheduling (computing), [ INFO.INFO-PL ] Computer Science [cs]/Programming Languages [cs.PL], 0103 physical sciences, 0202 electrical engineering, electronic engineering, information engineering, Electrical and Electronic Engineering, Parametric statistics, 010302 applied physics, [INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL], Scheduling, ACM : F.: Theory of Computation/F.1: COMPUTATION BY ABSTRACT DEVICES/F.1.1: Models of Computation, Static analysis, Computer Graphics and Computer-Aided Design, Throughput, 020202 computer hardware & architecture, Computer Science Applications, Latency, Linear approximation, Symbolic analysis, ACM : I.: Computing Methodologies/I.1: SYMBOLIC AND ALGEBRAIC MANIPULATION, ACM: I.: Computing Methodologies/I.1: SYMBOLIC AND ALGEBRAIC MANIPULATION, Compile time
Abstract: The synchronous dataflow model of computation is widely used to design embedded stream-processing applications under strict quality-of-service requirements (e.g., buffering size, throughput, input-output latency). The required analyses can either be performed at compile time (for design space exploration) or at runtime (for resource management and reconfigurable systems). However, these analyses have an exponential time complexity, which may cause a huge runtime overhead or make design space exploration unacceptably slow. In this article, we argue that symbolic analyses are more appropriate since they express the system performance as a function of parameters (i.e., input and output rates, execution times). Such functions can be quickly evaluated for each different configuration or checked with respect to different quality-of-service requirements. We provide symbolic analyses for computing the maximal throughput of acyclic synchronous dataflow graphs, the minimum required buffers for which as soon as possible (ASAP) scheduling achieves this throughput, and finally, the corresponding input-output latency of the graph. The article first investigates these problems for a single parametric edge. The results are extended to general acyclic graphs using linear approximation techniques. We assess the proposed analyses experimentally on both synthetic and real benchmarks.
Published: 2017

9. Actors may synchronize, safely! *

Author: Cosimo Laneve, Elena Giachino, Ludovic Henrio, Vincenzo Mastandrea, Department of Computer Science and Engineering [Bologna] (DISI), Alma Mater Studiorum Università di Bologna [Bologna] (UNIBO), Foundations of Component-based Ubiquitous Systems (FOCUS), Inria Sophia Antipolis - Méditerranée (CRISAM), Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Dipartimento di Informatica - Scienza e Ingegneria [Bologna] (DISI), Alma Mater Studiorum Università di Bologna [Bologna] (UNIBO)-Alma Mater Studiorum Università di Bologna [Bologna] (UNIBO), COMmunications, Réseaux, systèmes Embarqués et Distribués (Laboratoire I3S - COMRED), Laboratoire d'Informatique, Signaux, et Systèmes de Sophia Antipolis (I3S), Université Nice Sophia Antipolis (... - 2019) (UNS), COMUE Université Côte d'Azur (2015-2019) (COMUE UCA)-COMUE Université Côte d'Azur (2015-2019) (COMUE UCA)-Centre National de la Recherche Scientifique (CNRS)-Université Côte d'Azur (UCA)-Université Nice Sophia Antipolis (... - 2019) (UNS), COMUE Université Côte d'Azur (2015-2019) (COMUE UCA)-COMUE Université Côte d'Azur (2015-2019) (COMUE UCA)-Centre National de la Recherche Scientifique (CNRS)-Université Côte d'Azur (UCA), Université Nice Sophia Antipolis (1965 - 2019) (UNS), COMUE Université Côte d'Azur (2015-2019) (COMUE UCA)-COMUE Université Côte d'Azur (2015-2019) (COMUE UCA)-Centre National de la Recherche Scientifique (CNRS)-Université Côte d'Azur (UCA)-Université Nice Sophia Antipolis (1965 - 2019) (UNS), Giachino, Elena, Henrio, Ludovic, Laneve, Cosimo, Mastandrea, Vincenzo, Department of Computer Science and Engineering [Bologna] ( DISI ), Università di Bologna [Bologna] ( UNIBO ), Foundations of Component-based Ubiquitous Systems ( FOCUS ), Inria Sophia Antipolis - Méditerranée ( CRISAM ), Institut National de Recherche en Informatique et en Automatique ( Inria ) -Institut National de Recherche en Informatique et en Automatique ( Inria ) -Dipartimento di Informatica - Scienza e Ingegneria [Bologna] ( DISI ), Università di Bologna [Bologna] ( UNIBO ) -Università di Bologna [Bologna] ( UNIBO ), COMmunications, Réseaux, systèmes Embarqués et Distribués ( COMRED ), Laboratoire d'Informatique, Signaux, et Systèmes de Sophia Antipolis ( I3S ), Université Nice Sophia Antipolis ( UNS ), Université Côte d'Azur ( UCA ) -Université Côte d'Azur ( UCA ) -Centre National de la Recherche Scientifique ( CNRS ) -Université Nice Sophia Antipolis ( UNS ), and Université Côte d'Azur ( UCA ) -Université Côte d'Azur ( UCA ) -Centre National de la Recherche Scientifique ( CNRS )
Subjects: Process (engineering), Computer science, Distributed computing, 0102 computer and information sciences, 02 engineering and technology, 01 natural sciences, Synchronization, [ INFO.INFO-DC ] Computer Science [cs]/Distributed, Parallel, and Cluster Computing [cs.DC], Software, type system, [ INFO.INFO-PL ] Computer Science [cs]/Programming Languages [cs.PL], Computational Theory and Mathematic, 0202 electrical engineering, electronic engineering, information engineering, Feature (machine learning), Deadlock prevention algorithms, [INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL], business.industry, Deadlock detection, Computer Science Applications1707 Computer Vision and Pattern Recognition, Solver, 010201 computation theory & mathematics, behavioral types, 020201 artificial intelligence & image processing, Actor model, [INFO.INFO-DC]Computer Science [cs]/Distributed, Parallel, and Cluster Computing [cs.DC], business, Futures contract, Behavioral type
Abstract: International audience; We study deadlock detection in an actor model with wait-by-necessity synchronizations, a lightweight technique that synchronizes invocations when the corresponding values are strictly needed. This approach relies on the use of futures that are not given an explicit " Future " type. The approach we adopt allow the implicit synchronization on the availability of some value (where the producer of the value might be decided at runtime), whereas previous work allowed only explicit synchronization on the termination of a well-identified request. This way we are able to analyse the data-flow synchronization inherent to languages that feature wait-by-necessity. We provide a type-system and a solver inferring the type of a program so that deadlocks can be identified statically. As a consequence we can automatically verify the absence of deadlocks in actor programs with wait-by-necessity synchronizations.
Published: 2016

10. A Method for Invariant Generation for Polynomial Continuous Systems

Author: Andrew Sogokon, Khalil Ghorbal, André Platzer, Paul B. Jackson, School of Informatics [Edimbourg], University of Edinburgh, Modélisation hybride & conception par contrats pour les systèmes embarqués multi-physiques (HYCOMES), Inria Rennes – Bretagne Atlantique, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-LANGAGE ET GÉNIE LOGICIEL (IRISA-D4), Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA), Université de Rennes (UR)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Institut National de Recherche en Informatique et en Automatique (Inria)-Télécom Bretagne-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-Université de Rennes (UR)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Institut National de Recherche en Informatique et en Automatique (Inria)-Télécom Bretagne-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Télécom Bretagne-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS), Carnegie Mellon University [Pittsburgh] (CMU), This material is based upon work supported by the UK Engineering and Physical Sciences Research Council (EPSRC) under grants EP/I010335/1 and EP/J001058/1, the National Science Foundation by NSF CAREER Award CNS-1054246, NSF EXPEDITION CNS-0926181, CNS-0931985 and DARPA FA8750-12-2-0291., Barbara Jobstmann, K. Rustan M. Leino, CentraleSupélec-Télécom Bretagne-Université de Rennes 1 (UR1), Université de Rennes (UNIV-RENNES)-Université de Rennes (UNIV-RENNES)-Institut National de Recherche en Informatique et en Automatique (Inria)-École normale supérieure - Rennes (ENS Rennes)-Université de Bretagne Sud (UBS)-Centre National de la Recherche Scientifique (CNRS)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-CentraleSupélec-Télécom Bretagne-Université de Rennes 1 (UR1), Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA), Université de Rennes (UNIV-RENNES)-Université de Rennes (UNIV-RENNES)-École normale supérieure - Rennes (ENS Rennes)-Université de Bretagne Sud (UBS)-Centre National de la Recherche Scientifique (CNRS)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA), Jobstmann, Barbara, Leino, M. K. Rustan, Modélisation hybride & conception par contrats pour les systèmes embarqués multi-physiques ( HYCOMES ), Institut National de Recherche en Informatique et en Automatique ( Inria ) -Institut National de Recherche en Informatique et en Automatique ( Inria ) -LANGAGE ET GÉNIE LOGICIEL ( IRISA-D4 ), Institut de Recherche en Informatique et Systèmes Aléatoires ( IRISA ), CentraleSupélec-Université de Rennes 1 ( UR1 ), Université de Rennes ( UNIV-RENNES ) -Université de Rennes ( UNIV-RENNES ) -Télécom Bretagne-Institut National des Sciences Appliquées ( INSA ) -Institut National de Recherche en Informatique et en Automatique ( Inria ) -École normale supérieure - Rennes ( ENS Rennes ) -Centre National de la Recherche Scientifique ( CNRS ) -Université de Bretagne Sud ( UBS ) -CentraleSupélec-Université de Rennes 1 ( UR1 ), Université de Rennes ( UNIV-RENNES ) -Université de Rennes ( UNIV-RENNES ) -Télécom Bretagne-Institut National des Sciences Appliquées ( INSA ) -Institut National de Recherche en Informatique et en Automatique ( Inria ) -École normale supérieure - Rennes ( ENS Rennes ) -Centre National de la Recherche Scientifique ( CNRS ) -Université de Bretagne Sud ( UBS ) -Institut de Recherche en Informatique et Systèmes Aléatoires ( IRISA ), Université de Rennes ( UNIV-RENNES ) -Université de Rennes ( UNIV-RENNES ) -Télécom Bretagne-Institut National des Sciences Appliquées ( INSA ) -École normale supérieure - Rennes ( ENS Rennes ) -Centre National de la Recherche Scientifique ( CNRS ) -Université de Bretagne Sud ( UBS ), and Carnegie Mellon University [Pittsburgh] ( CMU )
Subjects: 0209 industrial biotechnology, Computer science, 02 engineering and technology, 020901 industrial engineering & automation, [INFO.INFO-FL]Computer Science [cs]/Formal Languages and Automata Theory [cs.FL], [ INFO.INFO-PL ] Computer Science [cs]/Programming Languages [cs.PL], 0202 electrical engineering, electronic engineering, information engineering, [INFO.INFO-SY]Computer Science [cs]/Systems and Control [cs.SY], Symbolic Computation, Abstraction, Invariant (mathematics), Formal verification, Formal Verification, [INFO.INFO-SC]Computer Science [cs]/Symbolic Computation [cs.SC], [INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL], Symbolic computation, [ INFO.INFO-SC ] Computer Science [cs]/Symbolic Computation [cs.SC], Algebra, Proof rule, Ordinary differential equation, [ INFO.INFO-FL ] Computer Science [cs]/Formal Languages and Automata Theory [cs.FL], Scalability, [ INFO.INFO-SY ] Computer Science [cs]/Systems and Control [cs.SY], 020201 artificial intelligence & image processing, Performance improvement, Algorithm
Abstract: International audience; This paper presents a method for generating semi-algebraic invariants for systems governed by non-linear polynomial ordinary differential equations under semi-algebraic evolution constraints. Based on the notion of discrete abstraction , our method eliminates unsoundness and unnecessary coarseness found in existing approaches for computing abstractions for non-linear continuous systems and is able to construct invariants with intricate boolean structure, in contrast to invariants typically generated using template-based methods. In order to tackle the state explosion problem associated with discrete abstraction, we present invariant generation algorithms that exploit sound proof rules for safety verification , such as differential cut (DC), and a new proof rule that we call differential divide-and-conquer (DDC), which splits the verification problem into smaller sub-problems. The resulting invariant generation method is observed to be much more scalable and efficient than the na¨ıvena¨ıve approach, exhibiting orders of magnitude performance improvement on many of the problems.
Published: 2016
Full Text: View/download PDF

11. The chemical approach to typestate-oriented programming

Author: Luca Padovani, Silvia Crafa, Dipartimento di Matematica [padova], Universita degli Studi di Padova, Dipartimento di Informatica [Torino], and Università degli studi di Torino ( UNITO )
Subjects: Computer science, Metaphor, Concurrency, media_common.quotation_subject, 0102 computer and information sciences, 02 engineering and technology, Behavioral types, Join calculus, Typestate, Software, computer.software_genre, 01 natural sciences, Typestate, Concurrency, Behavioral Types, Join Calculus, Object sharing, Simple (abstract algebra), [ INFO.INFO-PL ] Computer Science [cs]/Programming Languages [cs.PL], 0202 electrical engineering, electronic engineering, information engineering, Control (linguistics), media_common, Programming language, 020207 software engineering, Object (computer science), Computer Graphics and Computer-Aided Design, Join-calculus, Type theory, 010201 computation theory & mathematics, State (computer science), computer
Abstract: To appear in the proceedings of OOPSLA 2015; We study a novel approach to typestate-oriented programming based on the chemical metaphor: state and operations on objects are molecules of messages and state transformations are chemical reactions. This approach allows us to investigate typestate in an inherently concurrent setting, whereby objects can be accessed and modified concurrently by several processes, each potentially changing only part of their state. We introduce a simple behavioral type theory to express in a uniform way both the private and the public interfaces of objects, to describe and enforce structured object protocols consisting of possibilities, prohibitions, and obligations , and to control object sharing.
Published: 2015

12. Une approche hybride GPL-DSL pour transformer des modèles

Author: Jean-Christophe Bach, Formal islands: foundations and applications (PAREO), Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Department of Formal Methods (LORIA - FM), Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), Formal islands: foundations and applications ( PAREO ), Institut National de Recherche en Informatique et en Automatique ( Inria ) -Institut National de Recherche en Informatique et en Automatique ( Inria ) -Department of Formal Methods ( LORIA - FM ), Laboratoire Lorrain de Recherche en Informatique et ses Applications ( LORIA ), Institut National de Recherche en Informatique et en Automatique ( Inria ) -Université de Lorraine ( UL ) -Centre National de la Recherche Scientifique ( CNRS ) -Institut National de Recherche en Informatique et en Automatique ( Inria ) -Université de Lorraine ( UL ) -Centre National de la Recherche Scientifique ( CNRS ) -Laboratoire Lorrain de Recherche en Informatique et ses Applications ( LORIA ), Institut National de Recherche en Informatique et en Automatique ( Inria ) -Université de Lorraine ( UL ) -Centre National de la Recherche Scientifique ( CNRS ) -Université de Lorraine ( UL ) -Centre National de la Recherche Scientifique ( CNRS ), Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), and Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)
Subjects: models transformations, language, [INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL], Philosophy, java, 020207 software engineering, 02 engineering and technology, tom, EMF, Ecore, [ INFO.INFO-PL ] Computer Science [cs]/Programming Languages [cs.PL], 0202 electrical engineering, electronic engineering, information engineering, 020201 artificial intelligence & image processing, Humanities, transformation language
Abstract: Version définitive; National audience; Model Driven Engineering (MDE) advocates the use of model transformations in order to automate software development and its verification. Between operational and relational approaches, based on general purpose or domain specific languages, many models transformations tools have been developed. To ease and to speed up software development based on models transformations, we propose a method, an associated language and dedicated tooling. Our approach aims to bridge the gap between general purpose languages and domain specific ones in order to take benefit from both of the two worlds, increasing software quality. Our approach uses the Tom language which is a shallow extension of general purpose languages. Our proposal allows to write modular transformations whose code is reusable, and which are traceable.; L'ingénierie des modèles (IDM) plaide en faveur des transformations de modèles afin d'automatiser au maximum le développement logiciel et sa vérification. Entre approches opérationnelles et relationnelles, à base de langages dédiés ou généralistes, de nombreux outils de transformation de modèles existent dans le domaine. Pour faciliter et accélérer le développement logiciel basé sur les transformations de modèles, tout en assurant la qualité du logiciel, nous proposons une méthode ainsi qu'un langage associé et de l'outillage dédié. Notre approche se situe à la frontière des langages généralistes et des langages dédiés afin de pouvoir bénéficier du meilleur des deux mondes pour une qualité logicielle accrue. Elle s'appuie sur l'usage du langage Tom, qui est une extension de langages généralistes. Notre proposition permet d'écrire des transformations modulaires, dont le code est réutilisable, et qui sont traçables.
Published: 2013
Full Text: View/download PDF

13. Island Grammar-based Parsing using GLL and Tom

Author: Elizabeth Scott, Jean-Christophe Bach, MW Maarten Manders, Adrian Johnstone, Ali Afroozeh, Pierre-Etienne Moreau, Mark van den Brand, Eindhoven University of Technology [Eindhoven] ( TU/e ), Formal islands: foundations and applications ( PAREO ), Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique ( Inria ) -Institut National de Recherche en Informatique et en Automatique ( Inria ) -Department of Formal Methods ( LORIA - FM ), Laboratoire Lorrain de Recherche en Informatique et ses Applications ( LORIA ), Institut National de Recherche en Informatique et en Automatique ( Inria ) -Université de Lorraine ( UL ) -Centre National de la Recherche Scientifique ( CNRS ) -Institut National de Recherche en Informatique et en Automatique ( Inria ) -Université de Lorraine ( UL ) -Centre National de la Recherche Scientifique ( CNRS ) -Laboratoire Lorrain de Recherche en Informatique et ses Applications ( LORIA ), Institut National de Recherche en Informatique et en Automatique ( Inria ) -Université de Lorraine ( UL ) -Centre National de la Recherche Scientifique ( CNRS ) -Université de Lorraine ( UL ) -Centre National de la Recherche Scientifique ( CNRS ), Department of Computer Science, Royal Holloway [University of London] ( RHUL ), Eindhoven University of Technology [Eindhoven] (TU/e), Formal islands: foundations and applications (PAREO), Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Department of Formal Methods (LORIA - FM), Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), Royal Holloway [University of London] (RHUL), Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), and Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)
Subjects: Computer science, media_common.quotation_subject, parsing, 02 engineering and technology, Top-down parsing, computer.software_genre, Rule-based machine translation, [ INFO.INFO-PL ] Computer Science [cs]/Programming Languages [cs.PL], 0202 electrical engineering, electronic engineering, information engineering, Pattern matching, computer.programming_language, media_common, Parsing, [INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL], Grammar, Programming language, business.industry, 020207 software engineering, Python (programming language), island grammars, Tom, TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, High-level programming language, 020201 artificial intelligence & image processing, S-attributed grammar, Artificial intelligence, GLL, business, computer, Natural language processing, disambiguation
Abstract: International audience; Extending a language by embedding within it another language presents significant parsing challenges, especially if the embedding is recursive. The composite grammar is likely to be nondeterministic as a result of tokens that are valid in both the host and the embedded language. In this paper we examine the challenges of embedding the Tom language into a variety of general-purpose high level languages. Tom provides syntax and semantics for advanced pattern matching and tree rewriting facilities. Embedded Tom constructs are translated into the host language by a preprocessor, the output of which is a composite program written purely in the host language. Tom implementations exist for Java, C, C#, Python and Caml. The current parser is complex and difficult to maintain. In this paper, we describe how Tom can be parsed using island grammars implemented with the Generalised LL (GLL) parsing algorithm. The grammar is, as might be expected, ambiguous. Extracting the correct derivation relies on our disambiguation strategy which is based on pattern matching within the parse forest. We describe different classes of ambiguity and propose patterns for resolving them.
Published: 2012
Full Text: View/download PDF

14. XA2C Framework for XML Alteration/Adaptation

Author: Jacques Fayolle, Richard Chbeir, Gilbert Tekli, Dispositifs et Instrumentation en Optoélectronique et micro-ondes (DIOM), Université Jean Monnet [Saint-Étienne] (UJM), Laboratoire Electronique, Informatique et Image [UMR6306] (Le2i), Université de Bourgogne (UB)-École Nationale Supérieure d'Arts et Métiers (ENSAM), Arts et Métiers Sciences et Technologies, HESAM Université (HESAM)-HESAM Université (HESAM)-Arts et Métiers Sciences et Technologies, HESAM Université (HESAM)-HESAM Université (HESAM)-AgroSup Dijon - Institut National Supérieur des Sciences Agronomiques, de l'Alimentation et de l'Environnement-Centre National de la Recherche Scientifique (CNRS), Fayolle, Jacques, Dispositifs et Instrumentation en Optoélectronique et micro-ondes ( DIOM ), Université Jean Monnet [Saint-Étienne] ( UJM ), Laboratoire Electronique, Informatique et Image ( Le2i ), and Université de Bourgogne ( UB ) -AgroSup Dijon - Institut National Supérieur des Sciences Agronomiques, de l'Alimentation et de l'Environnement-Centre National de la Recherche Scientifique ( CNRS )
Subjects: [INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL], Database, Programming language, computer.internet_protocol, Computer science, 02 engineering and technology, computer.software_genre, [INFO.INFO-PL] Computer Science [cs]/Programming Languages [cs.PL], Set (abstract data type), Identification (information), Visual language, Data extraction, 020204 information systems, [ INFO.INFO-PL ] Computer Science [cs]/Programming Languages [cs.PL], 0202 electrical engineering, electronic engineering, information engineering, 020201 artificial intelligence & image processing, Mashup, Control (linguistics), Adaptation (computer science), computer, XML, ComputingMilieux_MISCELLANEOUS
Abstract: XML has crossed the borders of software engineering and has spread to other areas such as e-commerce, identification, information storage, instant messaging and others. It is used to communicate crucial data over these domains. Thus, allowing non-expert programmers to manipulate and control their XML data is essential. In the literature, this issue has been dealt with from 3 perspectives: (i) XML alteration/adaptation techniques requiring a certain level of expertise to be implemented and are not unified yet, (ii) mashups, which are not formally defined yet and are not specific to XML data, and (iii) XML-oriented visual languages based on structural transformations and data extraction mainly and not allowing XML textual data manipulations. In this paper, we discuss existing approaches and present our XA2C framework intended for both non-expert and expert programmers able to provide them with means to write/draw their XML data manipulation operations. The framework is designed in the combined spirits of both mashups and XMLoriented visual languages by defining a well-founded modular architecture similar to mashups and an XML-oriented visual functional composition language based on colored petri nets. The framework takes advantage of existing XML alteration/adaptation techniques by defining them as XML-oriented manipulation functions. A prototype called XA2C is developed and presented here with the set of tests conducted to validate our approach.
Published: 2010

15. The Third Rewrite Engines Competition

Author: Durán, F., Roldán, M., Bach, J.-C., Balland, E., Brand, van den, M.G.J., Cordy, J.R., Eker, S., Engelen, L.J.P., Jonge, de, M., Kalleberg, K.T., Kats, L.C.L., Moreau, P.-E., Visser, E., Ölveczky, P.C., Departamento Lenguajes y Ciencias de la Computación [Malaga] ( LCC ), Universidad de Málaga [Málaga], Formal islands: foundations and applications ( PAREO ), INRIA Lorraine, Institut National de Recherche en Informatique et en Automatique ( Inria ) -Institut National de Recherche en Informatique et en Automatique ( Inria ) -Laboratoire Lorrain de Recherche en Informatique et ses Applications ( LORIA ), Institut National de Recherche en Informatique et en Automatique ( Inria ) -Université Henri Poincaré - Nancy 1 ( UHP ) -Université Nancy 2-Institut National Polytechnique de Lorraine ( INPL ) -Centre National de la Recherche Scientifique ( CNRS ) -Université Henri Poincaré - Nancy 1 ( UHP ) -Université Nancy 2-Institut National Polytechnique de Lorraine ( INPL ) -Centre National de la Recherche Scientifique ( CNRS ), Programming Language Technology For Communication Services ( Phoenix ), Laboratoire Bordelais de Recherche en Informatique ( LaBRI ), Centre National de la Recherche Scientifique ( CNRS ) -École Nationale Supérieure d'Électronique, Informatique et Radiocommunications de Bordeaux (ENSEIRB)-Université Sciences et Technologies - Bordeaux 1-Université Bordeaux Segalen - Bordeaux 2-Centre National de la Recherche Scientifique ( CNRS ) -École Nationale Supérieure d'Électronique, Informatique et Radiocommunications de Bordeaux (ENSEIRB)-Université Sciences et Technologies - Bordeaux 1-Université Bordeaux Segalen - Bordeaux 2-Inria Bordeaux - Sud-Ouest, Institut National de Recherche en Informatique et en Automatique ( Inria ) -Institut National de Recherche en Informatique et en Automatique ( Inria ) -Handicap et système nerveux :Action, communication, interaction: rétablissement de la fonction et de la participation [Bordeaux] ( EA4136 ), UFR Sciences médicales 3 [Bordeaux]-Université de Bordeaux Ségalen [Bordeaux 2]-UFR Sciences médicales 3 [Bordeaux]-Université de Bordeaux Ségalen [Bordeaux 2], Department of Mathematics and Computer Science [Eindhoven], Eindhoven University of Technology [Eindhoven] ( TU/e ), Queen's University [Kingston], SRI International [Menlo Park] ( SRI ), Computer Engineering - Delft University of Technology ( CE ), Delft University of Technology ( TU Delft ), Department of Informatics, University of Bergen ( UIB ), Peter Csaba Ölveczky, Departamento Lenguajes y Ciencias de la Computación [Malaga] (LCC), Universidad de Málaga [Málaga] = University of Málaga [Málaga], Formal islands: foundations and applications (PAREO), Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université Henri Poincaré - Nancy 1 (UHP)-Université Nancy 2-Institut National Polytechnique de Lorraine (INPL)-Centre National de la Recherche Scientifique (CNRS)-Université Henri Poincaré - Nancy 1 (UHP)-Université Nancy 2-Institut National Polytechnique de Lorraine (INPL)-Centre National de la Recherche Scientifique (CNRS), Programming Language Technology For Communication Services (Phoenix), Laboratoire Bordelais de Recherche en Informatique (LaBRI), 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)-Inria Bordeaux - Sud-Ouest, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Handicap et système nerveux :Action, communication, interaction: rétablissement de la fonction et de la participation [Bordeaux] (EA4136), Eindhoven University of Technology [Eindhoven] (TU/e), Queen's University [Kingston, Canada], SRI International [Menlo Park] (SRI), Computer Engineering - Delft University of Technology (CE), Delft University of Technology (TU Delft), Department of Informatics [Bergen] (UiB), University of Bergen (UiB), Centre National de la Recherche Scientifique (CNRS)-Institut National Polytechnique de Lorraine (INPL)-Université Nancy 2-Université Henri Poincaré - Nancy 1 (UHP)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Institut National Polytechnique de Lorraine (INPL)-Université Nancy 2-Université Henri Poincaré - Nancy 1 (UHP), Handicap et système nerveux :Action, communication, interaction: rétablissement de la fonction et de la participation [Bordeaux] (EA4136), UFR Sciences médicales 3 [Bordeaux]-Université de Bordeaux Ségalen [Bordeaux 2]-UFR Sciences médicales 3 [Bordeaux]-Université de Bordeaux Ségalen [Bordeaux 2]-Inria Bordeaux - Sud-Ouest, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Bordelais de Recherche en Informatique (LaBRI), and 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)
Subjects: Theoretical computer science, [INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL], Computer science, Programming language, Automatic translation, Program transformation, 020207 software engineering, 0102 computer and information sciences, 02 engineering and technology, computer.software_genre, 01 natural sciences, Competition (economics), Concrete syntax, 010201 computation theory & mathematics, [ INFO.INFO-PL ] Computer Science [cs]/Programming Languages [cs.PL], 0202 electrical engineering, electronic engineering, information engineering, Rewriting, Computational linguistics, computer
Abstract: The original publication is available at www.springerlink.com; International audience; This paper presents the main results and conclusions of the Third Rewrite Engines Competition (REC III). This edition of the competition took place as part of the 8th Workshop on Rewriting Logic and its Applications (WRLA 2010), and the systems ASF+SDF, Maude, Stratego/XT, Tom, and TXL participated in it.
Published: 2010
Full Text: View/download PDF

16. A Mechanized Model of the Theory of Objects

Author: Ludovic Henrio, Florian Kammüller, Active objects, semantics, Internet and security ( OASIS ), Inria Sophia Antipolis - Méditerranée ( CRISAM ), Institut National de Recherche en Informatique et en Automatique ( Inria ) -Institut National de Recherche en Informatique et en Automatique ( Inria ) -COMmunications, Réseaux, systèmes Embarqués et Distribués ( COMRED ), Laboratoire d'Informatique, Signaux, et Systèmes de Sophia Antipolis ( I3S ), Université Nice Sophia Antipolis ( UNS ), Université Côte d'Azur ( UCA ) -Université Côte d'Azur ( UCA ) -Centre National de la Recherche Scientifique ( CNRS ) -Université Nice Sophia Antipolis ( UNS ), Université Côte d'Azur ( UCA ) -Université Côte d'Azur ( UCA ) -Centre National de la Recherche Scientifique ( CNRS ) -Laboratoire d'Informatique, Signaux, et Systèmes de Sophia Antipolis ( I3S ), Université Côte d'Azur ( UCA ) -Université Côte d'Azur ( UCA ) -Centre National de la Recherche Scientifique ( CNRS ), Technische Universität Berlin ( TUB ), Active objects, semantics, Internet and security (OASIS), Inria Sophia Antipolis - Méditerranée (CRISAM), Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-COMmunications, Réseaux, systèmes Embarqués et Distribués (Laboratoire I3S - COMRED), Laboratoire d'Informatique, Signaux, et Systèmes de Sophia Antipolis (I3S), Université Nice Sophia Antipolis (... - 2019) (UNS), COMUE Université Côte d'Azur (2015-2019) (COMUE UCA)-COMUE Université Côte d'Azur (2015-2019) (COMUE UCA)-Centre National de la Recherche Scientifique (CNRS)-Université Côte d'Azur (UCA)-Université Nice Sophia Antipolis (... - 2019) (UNS), COMUE Université Côte d'Azur (2015-2019) (COMUE UCA)-COMUE Université Côte d'Azur (2015-2019) (COMUE UCA)-Centre National de la Recherche Scientifique (CNRS)-Université Côte d'Azur (UCA)-Laboratoire d'Informatique, Signaux, et Systèmes de Sophia Antipolis (I3S), COMUE Université Côte d'Azur (2015-2019) (COMUE UCA)-COMUE Université Côte d'Azur (2015-2019) (COMUE UCA)-Centre National de la Recherche Scientifique (CNRS)-Université Côte d'Azur (UCA), Technische Universität Berlin (TU), Université Nice Sophia Antipolis (1965 - 2019) (UNS), COMUE Université Côte d'Azur (2015-2019) (COMUE UCA)-COMUE Université Côte d'Azur (2015-2019) (COMUE UCA)-Centre National de la Recherche Scientifique (CNRS)-Université Côte d'Azur (UCA)-Université Nice Sophia Antipolis (1965 - 2019) (UNS), and Technical University of Berlin / Technische Universität Berlin (TU)
Subjects: Theoretical computer science, Simply typed lambda calculus, [INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL], Programming language, Computer science, Proof assistant, HOL, 020207 software engineering, Distributed object, 0102 computer and information sciences, 02 engineering and technology, computer.software_genre, Mathematical proof, 01 natural sciences, Operational semantics, Functional calculus, TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, 010201 computation theory & mathematics, TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, [ INFO.INFO-PL ] Computer Science [cs]/Programming Languages [cs.PL], 0202 electrical engineering, electronic engineering, information engineering, Lambda calculus, computer, computer.programming_language
Abstract: In this paper we present a formalization of Abadi's and Cardelli's theory of ob jects in the interactive theorem prover Isabelle/HOL. Our motivation is to build a mechanized HOL-framework for the analysis of a functional calculus for distributed ob jects. In particular, we present (a) a formal model of ob jects and its operational semantics based on de Bruijn indices (b) a parallel reduction relation for ob jects (c) the proof of confluence for the theory of ob jects reusing Nipkow's HOL-framework for the lambda calculus. We expect this framework to be highly reusable and allow further development and mechanized proofs of various aspects of ob ject theory, e.g., distribution, aspect orientation, typing.
Published: 2007

17. Interval Propagation to Reason about Sets: Definition and Implementation of a Practical Language

Author: Carmen Gervet, UMR 228 Espace-Dev, Espace pour le développement, Institut de Recherche pour le Développement (IRD)-Université de Perpignan Via Domitia (UPVD)-Avignon Université (AU)-Université de La Réunion (UR)-Université de Montpellier (UM)-Université de Guyane (UG)-Université des Antilles (UA), Department of Computing [Imperial College London], Imperial College London, Institut de Recherche pour le Développement ( IRD ) -Université de Perpignan Via Domitia ( UPVD ) -Université Nice Sophia Antipolis ( UNS ), Université Côte d'Azur ( UCA ) -Université Côte d'Azur ( UCA ) -Université d'Avignon et des Pays de Vaucluse ( UAPV ) -Université de la Réunion ( UR ) -Université de Montpellier ( UM ) -Université de Guyane ( UG ) -Université des Antilles ( UA ), and Université de Guyane (UG)-Université des Antilles (UA)-Institut de Recherche pour le Développement (IRD)-Université de Perpignan Via Domitia (UPVD)-Avignon Université (AU)-Université de La Réunion (UR)-Université de Montpellier (UM)
Subjects: Infinite set, Theoretical computer science, relational set constraints, constraint programming language, 0102 computer and information sciences, 02 engineering and technology, Interval (mathematics), computer.software_genre, 01 natural sciences, [INFO.INFO-AI]Computer Science [cs]/Artificial Intelligence [cs.AI], Set (abstract data type), CSP, Artificial Intelligence, [ INFO.INFO-PL ] Computer Science [cs]/Programming Languages [cs.PL], Constraint logic programming, 0202 electrical engineering, electronic engineering, information engineering, Constraint programming, interval propagation, Discrete Mathematics and Combinatorics, [ INFO.INFO-AI ] Computer Science [cs]/Artificial Intelligence [cs.AI], Logic programming, Mathematics, [INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL], Programming language, consistency techniques, Constraint satisfaction, Computational Theory and Mathematics, 010201 computation theory & mathematics, finite set domains, 020201 artificial intelligence & image processing, CLP, computer, Software, Active set method
Abstract: International audience; Local consistency techniques have been introduced in logic programming in order to extend the application domain of logic programming languages. The existing languages based on these techniques consider arithmetic constraints applied to variables ranging over finite integer domains. This makes difficult a natural and concise modelling as well as an efficient solving of a class of N P-complete combinatorial search problems dealing with sets. To overcome these problems, we propose a solution which consists in extending the notion of integer domains to that of set domains (sets of sets). We specify a set domain by an interval whose lower and upper bounds are known sets, ordered by set inclusion. We define the formal and practical framework of a new constraint logic programming language over set domains, called Conjunto. Conjunto comprises the usual set operation symbols(\ n), and the set inclusion relation (). Set expressions built using the operation symbols are interpreted as relations (s s 1 = s 2 ,...). In addition, Conjunto provides us with a set of constraints called graduated constraints (e.g. the set cardinality) which map sets onto arithmetic terms. This allows us to handle optimization problems by applying a cost function to the quantiiable, i.e., arithmetic, terms which are associated to set terms. The constraint solving in Conjunto is based on local consistency techniques using interval reasoning which are extended to handle set constraints. The main contribution of this paper concerns the formal deenition of the language and its design and implementation as a practical language.
Published: 1997
Full Text: View/download PDF

Catalog

Books, media, physical & digital resources

See catalog results

Searchworks

Select search scope, currently: Articles

Catalog

books, media & more in Jio Institute collections

Articles

journal articles & other e-resources

Refine your results

17 results on '"[ INFO.INFO-PL ] Computer Science [cs]/Programming Languages [cs.PL]"'

1. Towards Certified Meta-Programming with Typed Template-Coq

2. Extending Timbuk to Verify Functional Programs

3. Implementing Modular Class-based Reuse Mechanisms on Top of a Single Inheritance VM

4. Foundations of Dependent Interoperability

5. Scalable Machine Learning for Predicting At-Risk Profiles Upon Hospital Admission

6. A polyhedral compilation framework for loops with dynamic data-dependent bounds

7. A Survey of Parametric Dataflow Models of Computation

8. Symbolic Analyses of Dataflow Graphs

9. Actors may synchronize, safely! *

10. A Method for Invariant Generation for Polynomial Continuous Systems

11. The chemical approach to typestate-oriented programming

12. Une approche hybride GPL-DSL pour transformer des modèles

13. Island Grammar-based Parsing using GLL and Tom

14. XA2C Framework for XML Alteration/Adaptation

15. The Third Rewrite Engines Competition

16. A Mechanized Model of the Theory of Objects

17. Interval Propagation to Reason about Sets: Definition and Implementation of a Practical Language

Catalog

Searchworks

Select search scope, currently: Articles Catalog books, media & more in Jio Institute collections Articles journal articles & other e-resources

Search

Search Constraints

Refine your results

Search Limiters

Topic

Publication Year Range

Language

Database

Publisher

17 results on '"[ INFO.INFO-PL ] Computer Science [cs]/Programming Languages [cs.PL]"'

Search Results

Catalog

Select search scope, currently: Articles

Catalog

books, media & more in Jio Institute collections

Articles

journal articles & other e-resources