Search

Your search keyword '"Centro Franco Argentino de Ciencias de la Información y de Sistemas [Rosario] (CIFASIS)"' showing total 16 results
Start Over Author "Centro Franco Argentino de Ciencias de la Información y de Sistemas [Rosario] (CIFASIS)"
16 results on '"Centro Franco Argentino de Ciencias de la Información y de Sistemas [Rosario] (CIFASIS)"'

1. A Lagrangian Approach for Aggregative Mean Field Games of Controls with Mixed and Final Constraints

Author

J. Frédéric Bonnans, Justina Gianatti, Laurent Pfeiffer, Controle, Optimisation, modèles, Méthodes et Applications pour les Systèmes Dynamiques non linéaires (COMMANDS), Centre de Mathématiques Appliquées - Ecole Polytechnique (CMAP), École polytechnique (X)-Centre National de la Recherche Scientifique (CNRS)-École polytechnique (X)-Centre National de la Recherche Scientifique (CNRS)-Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Universidad Nacional de Rosario [Santa Fe], Centro Franco Argentino de Ciencias de la Información y de Sistemas [Rosario] (CIFASIS), Consejo Nacional de Investigaciones Científicas y Técnicas [Buenos Aires] (CONICET)-Universidad Nacional de Rosario [Santa Fe], Dynamical Interconnected Systems in COmplex Environments (DISCO), Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire des signaux et systèmes (L2S), CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS), and Universidad Nacional de Rosario [Santa Fe]-Consejo Nacional de Investigaciones Científicas y Técnicas [Buenos Aires] (CONICET)

Subjects
Computer Science::Computer Science and Game Theory, aggregative games, Control and Optimization, Optimization and Control (math.OC), Applied Mathematics, Lagrangian equilibria, FOS: Mathematics, TheoryofComputation_GENERAL, [MATH.MATH-OC]Mathematics [math]/Optimization and Control [math.OC], constrained optimal control, Mathematics - Optimization and Control, Mean field games of controls
Abstract

The objective of this paper is to analyze the existence of equilibria for a class of deterministic mean field games of controls. The interaction between players is due to both a congestion term and a price function which depends on the distributions of the optimal strategies. Moreover, final state and mixed state-control constraints are considered, the dynamics being nonlinear and affine with respect to the control. The existence of equilibria is obtained by Kakutani's theorem, applied to a fixed point formulation of the problem. Finally, uniqueness results are shown under monotonicity assumptions.

Published
2023
Full Text
View/download PDF

2. An algorithm for computing the generalized interaction index for k-maxitive fuzzy measures

Author

Pilar Bulacio, Tewfik Sari, Serge Guillaume, Javier Murillo, Centro Franco Argentino de Ciencias de la Información y de Sistemas [Rosario] (CIFASIS), Consejo Nacional de Investigaciones Científicas y Técnicas [Buenos Aires] (CONICET)-Universidad Nacional de Rosario [Santa Fe], Information – Technologies – Analyse Environnementale – Procédés Agricoles (UMR ITAP), Institut national d’études supérieures agronomiques de Montpellier (Montpellier SupAgro), and Institut national d'enseignement supérieur pour l'agriculture, l'alimentation et l'environnement (Institut Agro)-Institut national d'enseignement supérieur pour l'agriculture, l'alimentation et l'environnement (Institut Agro)-Institut National de Recherche pour l’Agriculture, l’Alimentation et l’Environnement (INRAE)

Subjects
Statistics and Probability, Computer science, [INFO.INFO-DS]Computer Science [cs]/Data Structures and Algorithms [cs.DS], General Engineering, 02 engineering and technology, Fuzzy logic, Shapley index, Artificial Intelligence, interaction index, 020204 information systems, 0202 electrical engineering, electronic engineering, information engineering, 020201 artificial intelligence & image processing, Interaction index, k-maxitive measures, Algorithm, Fuzzy measures
Abstract

International audience; Fuzzy measures are used for modeling interactions between a set of elements. Simplified fuzzy measures, as k-maxitive measures, were proposed in the literature for complexity and semantic considerations. In order to analyze the importance of a coalition in the fuzzy measure, the use of indices is required. This work focuses on the generalized interaction index, gindex. Its computation requires many resources in both time and space. Following the efforts to reduce the complexity of fuzzy measure identification, this work presents two algorithms to compute the gindex for k-maxitive measures. The structure of k-maxitive measures makes possible to compute the gindex considering the coalitions at level k and, for each of them, the number of coalitions sharing the same coefficient (called inheritors). The first algorithm deals with the space complexity and the second one also optimizes the runtime by not generating, but only counting, the number of inheritors. While counting the number of descendants is easy, this is not the case for the number of inheritors due to all the inheritors of previous considered coalitions have to be taken into account. The two proposed algorithms are tested with synthetic k-maxitive measures showing that the second algorithm is around 4 times faster than the first one.

Published
2020
Full Text
View/download PDF

3. SteelCore: An Extensible Concurrent Separation Logic for Effectful Dependently Typed Programs

Author

Aseem Rastogi, Guido Martínez, Aymeric Fromherz, Denis Merigoux, Danel Ahman, Nikhil Swamy, Microsoft Research [Redmond], Microsoft Corporation [Redmond, Wash.], Microsoft Research India [Bangalore], Microsoft Research, Carnegie Mellon University [Pittsburgh] (CMU), Programming securely with cryptography (PROSECCO), Inria de Paris, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), University of Ljubljana, Centro Franco Argentino de Ciencias de la Información y de Sistemas [Rosario] (CIFASIS), Consejo Nacional de Investigaciones Científicas y Técnicas [Buenos Aires] (CONICET)-Universidad Nacional de Rosario [Santa Fe], Aymeric Fromherz’s and Denis Merigoux’s work was supported in part by internships at Microsoft Research. Aymeric Fromherz was also funded by the Department of the Navy, Office of Naval Research under Grant no. N00014-18-1-2892. Denis Merigoux was also funded by ERC ConsolidatorGrant CIRCUS no. 683032. Danel Ahman’s work was supported in part by the Microsoft Research Visiting Researcher program. He has also received funding from the European Union’s Horizon 2020 research and innovation programme under the Marie Skłodowska-Curie grant agreement no. 834146., Programming securely with cryptography (PROSECCO ), and Universidad Nacional de Rosario [Santa Fe]-Consejo Nacional de Investigaciones Científicas y Técnicas [Buenos Aires] (CONICET)

Subjects
FOS: Computer and information sciences, Computer science, Semantics (computer science), Separation Logic, Concurrency, 0102 computer and information sciences, 02 engineering and technology, Separation logic, computer.software_genre, CONCURRENCY, 01 natural sciences, purl.org/becyt/ford/1 [https], Denotation, SEPARATION LOGIC, 0202 electrical engineering, electronic engineering, information engineering, Concurrent computing, Program Proofs, PROGRAM PROOFS, Layer (object-oriented design), Safety, Risk, Reliability and Quality, [INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL], Computer Science - Programming Languages, Programming language, Proof assistant, 020207 software engineering, purl.org/becyt/ford/1.2 [https], Type theory, 010201 computation theory & mathematics, computer, Software, Programming Languages (cs.PL)
Abstract

Much recent research has been devoted to modeling effects within type theory. Building on this work, we observe that effectful type theories can provide a foundation on which to build semantics for more complex programming constructs and program logics, extending the reasoning principles that apply within the host effectful type theory itself. Concretely, our main contribution is a semantics for concurrent separation logic (CSL) within the F* proof assistant in a manner that enables dependently typed, effectful F* programs to make use of concurrency and to be specified and verified using a full-featured, extensible CSL. In contrast to prior approaches, we directly derive the partial-correctness Hoare rules for CSL from the denotation of computations in the effectful semantics of non-deterministically interleaved atomic actions. Demonstrating the flexibility of our semantics, we build generic, verified libraries that support various concurrency constructs, ranging from dynamically allocated, storable spin locks, to protocol-indexed channels. We conclude that our effectful semantics provides a simple yet expressive basis on which to layer domain-specific languages and logics for verified, concurrent programming., ICFP 2020 camera-ready version

Published
2021
Full Text
View/download PDF

4. Steel: proof-oriented programming in a dependently typed concurrent separation logic

Author

Nikhil Swamy, Tahina Ramananandro, Guido Martínez, Aymeric Fromherz, Aseem Rastogi, Denis Merigoux, Sydney Gibson, Institut National de Recherche en Informatique et en Automatique (Inria), Carnegie Mellon University [Silicon Valley], Microsoft Research India [Bangalore], Microsoft Research, Centro Franco Argentino de Ciencias de la Información y de Sistemas [Rosario] (CIFASIS), Consejo Nacional de Investigaciones Científicas y Técnicas [Buenos Aires] (CONICET)-Universidad Nacional de Rosario [Santa Fe], Programming securely with cryptography (PROSECCO), Inria de Paris, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), and Aymeric Fromherz’s and Sydney Gibson’s work was supported in part by grants from the Intel Corporation, the Alfred P. Sloan Foundation, and the Department of the Navy, Office of Naval Research under Grant No. N00014-18-1-2892. Aymeric Fromherz was also supported in part by an internship at Microsoft Research. Sydney Gibson was also funded by the National Science Founda-tion Graduate Research Fellowship Program under Grant No. DGE1745016. Denis Merigoux’s work was partially supported by the European Research Council under the CIRCUS Consolidator Grant Agreement (683032).

Subjects
[INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL], Unification, Computer science, Programming language, Modulo, Concurrency, Proof assistant, 020207 software engineering, 02 engineering and technology, Separation logic, Hoare logic, computer.software_genre, Mathematical proof, 020204 information systems, 0202 electrical engineering, electronic engineering, information engineering, Session (computer science), Safety, Risk, Reliability and Quality, computer, Software
Abstract

Steel is a language for developing and proving concurrent programs embedded in F ⋆ , a dependently typed programming language and proof assistant. Based on SteelCore, a concurrent separation logic (CSL) formalized in F ⋆ , our work focuses on exposing the proof rules of the logic in a form that enables programs and proofs to be effectively co-developed. Our main contributions include a new formulation of a Hoare logic of quintuples involving both separation logic and first-order logic, enabling efficient verification condition (VC) generation and proof discharge using a combination of tactics and SMT solving. We relate the VCs produced by our quintuple system to solving a system of associativity-commutativity (AC) unification constraints and develop tactics to (partially) solve these constraints using AC-matching modulo SMT-dischargeable equations. Our system is fully mechanized and implemented in F ⋆ . We evaluate it by developing several verified programs and libraries, including various sequential and concurrent linked data structures, proof libraries, and a library for 2-party session types. Our experience leads us to conclude that our system enables a mixture of automated and interactive proof, making it productive to build programs foundationally verified against a highly expressive, state-of-the-art CSL.

Published
2021
Full Text
View/download PDF

5. Optimal control techniques based on infection age for the study of the COVID-19 epidemic

Author

Justina Gianatti, Joseph Frédéric Bonnans, Controle, Optimisation, modèles, Méthodes et Applications pour les Systèmes Dynamiques non linéaires (COMMANDS), Centre de Mathématiques Appliquées - Ecole Polytechnique (CMAP), École polytechnique (X)-Centre National de la Recherche Scientifique (CNRS)-École polytechnique (X)-Centre National de la Recherche Scientifique (CNRS)-Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Centro Franco Argentino de Ciencias de la Información y de Sistemas [Rosario] (CIFASIS), Universidad Nacional de Rosario [Santa Fe]-Consejo Nacional de Investigaciones Científicas y Técnicas [Buenos Aires] (CONICET), Universidad Nacional de Rosario [Santa Fe], Consejo Nacional de Investigaciones Científicas y Técnicas [Buenos Aires] (CONICET)-Universidad Nacional de Rosario [Santa Fe], and Centre National de la Recherche Scientifique (CNRS)-École polytechnique (X)-Centre National de la Recherche Scientifique (CNRS)-École polytechnique (X)-Inria Saclay - Ile de France

Subjects
0209 industrial biotechnology, Coronavirus disease 2019 (COVID-19), Computer science, Population, 02 engineering and technology, epidemic modelling, 03 medical and health sciences, optimal control, 020901 industrial engineering & automation, Modelling and Simulation, Statistics, [MATH]Mathematics [math], education, 030304 developmental biology, 0303 health sciences, education.field_of_study, age-structured systems, Applied Mathematics, Infection age, COVID-19, Optimal control, Term (time), Variable (computer science), Death toll, Modeling and Simulation, confinement, SIR epidemic models, [MATH.MATH-OC]Mathematics [math]/Optimization and Control [math.OC], Constant (mathematics)
Abstract

International audience; We propose a model for the COVID-19 epidemic where the population is partitioned into classes corresponding to ages (that remain constant during the epidemic). The main feature is to take into account the infection age of the infected population. This allows to better simulate the infection propagation that crucially depend on the infection age. We discuss how to compute the coefficients from data available in the future, and introduce a confinement variable as control. The cost function is a compromise between confinement cost, hospitalization peak and the death toll. Our numerical experiments allow to evaluate the interest of confinement varying with age classes.

Published
2020
Full Text
View/download PDF

6. Formalizing the Face Lattice of Polyhedra

Author

Xavier Allamigeon, Pierre-Yves Strub, Ricardo D. Katz, TROPICAL (TROPICAL), Centre de Mathématiques Appliquées - Ecole Polytechnique (CMAP), École polytechnique (X)-Centre National de la Recherche Scientifique (CNRS)-École polytechnique (X)-Centre National de la Recherche Scientifique (CNRS)-Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Centro Franco Argentino de Ciencias de la Información y de Sistemas [Rosario] (CIFASIS), Consejo Nacional de Investigaciones Científicas y Técnicas [Buenos Aires] (CONICET)-Universidad Nacional de Rosario [Santa Fe], Laboratoire d'informatique de l'École polytechnique [Palaiseau] (LIX), Centre National de la Recherche Scientifique (CNRS)-École polytechnique (X), École polytechnique (X)-Centre National de la Recherche Scientifique (CNRS), Allamigeon, Xavier, ANR-18-CE25-0014,scrypt,Compilation sécurisée de primitives cryptographiques(2018), ANR-17-CE40-0018,CAPPS,Analyse Combinatoire de Polytopes et de Subdivisions Polyédrales(2017), and ANR-11-LABX-0056,LMH,LabEx Mathématique Hadamard(2011)

Subjects
FOS: Computer and information sciences, Computer Science - Logic in Computer Science, [INFO.INFO-LO] Computer Science [cs]/Logic in Computer Science [cs.LO], Theoretical computer science, General Computer Science, Computer science, Face lattice, 0102 computer and information sciences, Computer Science::Computational Geometry, 01 natural sciences, Article, Theoretical Computer Science, Polyhedron, Linear programming, Lattice (order), [MATH.MATH-CO]Mathematics [math]/Combinatorics [math.CO], FOS: Mathematics, Mathematics - Combinatorics, Mathematics::Metric Geometry, Simplex method, 0101 mathematics, Mathematics - Optimization and Control, ComputingMilieux_MISCELLANEOUS, business.industry, 010102 general mathematics, Proof assistant, Regular polygon, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], [MATH.MATH-OC] Mathematics [math]/Optimization and Control [math.OC], Usability, Logic in Computer Science (cs.LO), [MATH.MATH-CO] Mathematics [math]/Combinatorics [math.CO], Optimization and Control (math.OC), 010201 computation theory & mathematics, Formal- ization of mathematics, Combinatorics (math.CO), [MATH.MATH-OC]Mathematics [math]/Optimization and Control [math.OC], business, Convex polyhedra, MathematicsofComputing_DISCRETEMATHEMATICS
Abstract

23 pages, 4 figures, minor revision. Extended version of hal-0315165.; Faces play a central role in the combinatorial and computational aspects of polyhedra. In this paper, we present the first formalization of faces of polyhedra in the proof assistant Coq. This builds on the formalization of a library providing the basic constructions and operations over polyhedra, including projections, convex hulls and images under linear maps. Moreover, we design a special mechanism which automatically introduces an appropriate representation of a polyhedron or a face, depending on the context of the proof. We demonstrate the usability of this approach by establishing some of the most important combinatorial properties of faces, namely that they constitute a family of graded atomistic and coatomistic lattices closed under interval sublattices. We also prove a theorem due to Balinski on the d-connectedness of the adjacency graph of polytopes of dimension d.

Published
2020
Full Text
View/download PDF

7. Monads with merging

Author

Rivas, Exequiel, Jaskelioff, Mauro, Programming securely with cryptography (PROSECCO ), Inria de Paris, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Universidad Nacional de Rosario [Santa Fe], Centro Franco Argentino de Ciencias de la Información y de Sistemas [Rosario] (CIFASIS), Universidad Nacional de Rosario [Santa Fe]-Consejo Nacional de Investigaciones Científicas y Técnicas [Buenos Aires] (CONICET), Rivas Gadda, Exequiel, Programming securely with cryptography (PROSECCO), and Consejo Nacional de Investigaciones Científicas y Técnicas [Buenos Aires] (CONICET)-Universidad Nacional de Rosario [Santa Fe]

Subjects
Process Algebra, Monads, [INFO.INFO-LO] Computer Science [cs]/Logic in Computer Science [cs.LO], TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, Bimonoids, TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, Computer Science::Logic in Computer Science, Mathematics::Category Theory, Concurrency, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO]
Abstract

Monoids are one of the simplest theories in which we can compose elements of a set. Similarly, monads have been used extensively to treat composition of effectful code and its denotational semantics. During the last forty years the theory of monoids has been extended with diverse merge-like operators. In this article, we replicate several of these extensions at the level of monads. Building on a well-known relation between monads and monoids, we introduce monads with additional structure that account for merging. We show how monads with merging generalise and relate to models for well-known algebraic theories for concurrency such as classic process algebras and the more recent concurrent monoids. With these results, we aim to facilitate the generalisation and comparison of different approaches to concurrency.

Published
2019

8. A multi-target compiler for CML-DEVS

Author

Maximiliano Cristiá, Claudia Frydman, Diego A. Hollmann, Laboratoire d'Informatique et Systèmes (LIS), Université de Toulon (UTLN)-Centre National de la Recherche Scientifique (CNRS)-Aix Marseille Université (AMU), Modèles et Formalismes à Evénements Discrets (MOFED), Université de Toulon (UTLN)-Centre National de la Recherche Scientifique (CNRS)-Aix Marseille Université (AMU)-Université de Toulon (UTLN)-Centre National de la Recherche Scientifique (CNRS)-Aix Marseille Université (AMU), Centro Franco Argentino de Ciencias de la Información y de Sistemas [Rosario] (CIFASIS), Consejo Nacional de Investigaciones Científicas y Técnicas [Buenos Aires] (CONICET)-Universidad Nacional de Rosario [Santa Fe], Aix Marseille Université (AMU)-Université de Toulon (UTLN)-Centre National de la Recherche Scientifique (CNRS), and Aix Marseille Université (AMU)-Université de Toulon (UTLN)-Centre National de la Recherche Scientifique (CNRS)-Aix Marseille Université (AMU)-Université de Toulon (UTLN)-Centre National de la Recherche Scientifique (CNRS)

Subjects
020203 distributed computing, 021103 operations research, DEVS, ComputingMethodologies_SIMULATIONANDMODELING, business.industry, Computer science, Programming language, ComputingMilieux_PERSONALCOMPUTING, 0211 other engineering and technologies, 02 engineering and technology, Modular design, Systems modeling, computer.software_genre, Computer Graphics and Computer-Aided Design, [INFO.INFO-MO]Computer Science [cs]/Modeling and Simulation, Formalism (philosophy of mathematics), Multi target, Modeling and Simulation, 0202 electrical engineering, electronic engineering, information engineering, Compiler, business, computer, Software, ComputingMilieux_MISCELLANEOUS
Abstract

Discrete Event System Specification (DEVS) is a modular and hierarchical formalism for system modeling and simulation. DEVS models can be mathematically described; simulation is performed by tools called concrete simulators. Concerning atomic DEVS models, each concrete simulator has its own input language which is, essentially, a general-purpose programming language (such as Java or C++). Hence, once engineers have written the mathematical model, they need to manually translate it into the input language of the concrete simulator of their choice. In this paper we present a multi-target compiler for atomic DEVS models written in CML-DEVS, a mathematics-based DEVS modeling language. This multi-target compiler is able to compile a CML-DEVS model to the input languages of the PowerDEVS and DEVS-Suite concrete simulators. In this way, the CML-DEVS compiler frees engineers from the manual translation of their mathematical models. In fact, the same mathematical model can be simulated on both simulators by simply recompiling the model. The CML-DEVS multi-target compiler can be easily extended to produce code for other concrete simulators.

Published
2019
Full Text
View/download PDF

9. Observer-based Controller for an Electric Vehicle with Hybrid Energy Storage

Author

Gildas Besancon, Ignacio RubioScola, Diego Feroldi, Mauro Patrone, Centro Franco Argentino de Ciencias de la Información y de Sistemas [Rosario] (CIFASIS), Consejo Nacional de Investigaciones Científicas y Técnicas [Buenos Aires] (CONICET)-Universidad Nacional de Rosario [Santa Fe], GIPSA - Systèmes non linéaires et complexité (GIPSA-SYSCO), Département Automatique (GIPSA-DA), Grenoble Images Parole Signal Automatique (GIPSA-lab ), Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Institut Polytechnique de Grenoble - Grenoble Institute of Technology-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 )-Institut Polytechnique de Grenoble - Grenoble Institute of Technology-Centre National de la Recherche Scientifique (CNRS)-Université Grenoble Alpes [2016-2019] (UGA [2016-2019])-Grenoble Images Parole Signal Automatique (GIPSA-lab ), Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Institut Polytechnique de Grenoble - Grenoble Institute of Technology-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 )-Institut Polytechnique de Grenoble - Grenoble Institute of Technology-Centre National de la Recherche Scientifique (CNRS)-Université Grenoble Alpes [2016-2019] (UGA [2016-2019]), and Besancon, Gildas

Subjects
0209 industrial biotechnology, business.product_category, Observer (quantum physics), Computer science, Energy management, 020209 energy, 02 engineering and technology, Kalman filter, [SPI.AUTO]Engineering Sciences [physics]/Automatic, [SPI.AUTO] Engineering Sciences [physics]/Automatic, 020901 industrial engineering & automation, Filter (video), Control theory, Electric vehicle, 0202 electrical engineering, electronic engineering, information engineering, Observability, business, Driving cycle, ComputingMilieux_MISCELLANEOUS
Abstract

In this work, we present an observer-based controller for an electric vehicle (EV) with hybrid energy storage system (HESS). We use a passivity-based controller, that relies on an observer to reduce the number of sensors, filter measured variables and estimate the current demanded by the vehicle. The observer chosen is a Kalman-Like observer design for nonuniformly observable systems that rely on persistent input to guarantee the system observability. Illustrations from numerical simulations show the performance of the control strategy during a standard driving cycle.

Published
2018

10. A French-Spanish Multimodal Speech Communication Corpus Incorporating Acoustic Data, Facial, Hands and Arms Gestures Information

Author

Bernard Girau, Mauricio Cerda, Juan Carlos Gómez, Lucas D. Terissi, Nancy Hitschfeld-Kahler, Rodrigo Galvez, Slim Ouni, Gonzalo D. Sad, Centro Franco Argentino de Ciencias de la Información y de Sistemas [Rosario] (CIFASIS), Consejo Nacional de Investigaciones Científicas y Técnicas [Buenos Aires] (CONICET)-Universidad Nacional de Rosario [Santa Fe], Laboratory for Scientific Image Analysis (SCIAN), Biomedical Neuroscience Institute, Speech Modeling for Facilitating Oral-Based Communication (MULTISPEECH), 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 Natural Language Processing & Knowledge Discovery (LORIA - NLPKD), 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), Universidad de Santiago de Chile [Santiago] (USACH), Bio-Inspired, Situated and Cellular Unconventional Information Technologies (BISCUIT), Department of Complex Systems, Artificial Intelligence & Robotics (LORIA - AIS), 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), Universidad Nacional de Rosario [Santa Fe]-Consejo Nacional de Investigaciones Científicas y Técnicas [Buenos Aires] (CONICET), 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), 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)-Institut National de Recherche en Informatique et en Automatique (Inria)

Subjects
Computer science, Head (linguistics), Speech recognition, media_common.quotation_subject, multimodal corpora, [SHS.INFO]Humanities and Social Sciences/Library and information sciences, multimodal speech, Face (sociological concept), [SCCO.COMP]Cognitive science/Computer science, 02 engineering and technology, [INFO.INFO-AI]Computer Science [cs]/Artificial Intelligence [cs.AI], [INFO.INFO-TS]Computer Science [cs]/Signal and Image Processing, Duration (music), human-computer interaction, 020204 information systems, 0202 electrical engineering, electronic engineering, information engineering, Natural (music), 020201 artificial intelligence & image processing, Conversation, Speech communication, [INFO.INFO-HC]Computer Science [cs]/Human-Computer Interaction [cs.HC], [SHS.LANGUE]Humanities and Social Sciences/Linguistics, media_common, Gesture
Abstract

International audience; A Bilingual Multimodal Speech Communication Corpus incorporating acoustic data as well as visual data related to face, hands and arms gestures during speech, is presented in this paper. This corpus comprises different speaking modalities, including scripted text speech, natural conversation, and free speech. The corpus has been compiled in two different languages , viz., French and Spanish. The experimental setups for the recording of the corpus, the acquisition protocols, and the employed equipment are described. Statistics regarding the number and gender of the speakers, number of words, number of sentences, and duration of the recording sessions, are also provided. Preliminary results from the analysis of the correlation among speech, head and hand movements during spontaneous speech are also presented in this paper, showing that acoustic prosodic features are related with head and hand gestures .

Published
2018

11. Condition numbers of stochastic mean payoff games and what they say about nonarchimedean semidefinite programming

Author

Allamigeon, Xavier, Gaubert, Stephane, Katz, Ricardo, Skomra, Mateusz, TROPICAL (TROPICAL), Centre de Mathématiques Appliquées - Ecole Polytechnique (CMAP), École polytechnique (X)-Centre National de la Recherche Scientifique (CNRS)-École polytechnique (X)-Centre National de la Recherche Scientifique (CNRS)-Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), École polytechnique (X)-Centre National de la Recherche Scientifique (CNRS), Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria), Centro Franco Argentino de Ciencias de la Información y de Sistemas [Rosario] (CIFASIS), Universidad Nacional de Rosario [Santa Fe]-Consejo Nacional de Investigaciones Científicas y Técnicas [Buenos Aires] (CONICET), and Consejo Nacional de Investigaciones Científicas y Técnicas [Buenos Aires] (CONICET)-Universidad Nacional de Rosario [Santa Fe]

Subjects
FOS: Computer and information sciences, Computer Science::Computer Science and Game Theory, Computer Science - Computer Science and Game Theory, Optimization and Control (math.OC), FOS: Mathematics, Mathematics - Combinatorics, [MATH.MATH-OC]Mathematics [math]/Optimization and Control [math.OC], Combinatorics (math.CO), Mathematics - Optimization and Control, Computer Science and Game Theory (cs.GT)
Abstract

Semidefinite programming can be considered over any real closed field, including fields of Puiseux series equipped with their nonarchimedean valuation. Nonarchimedean semidefinite programs encode parametric families of classical semidefinite programs, for sufficiently large values of the parameter. Recently, a correspondence has been established between nonarchimedean semidefinite programs and stochastic mean payoff games with perfect information. This correspondence relies on tropical geometry. It allows one to solve generic nonarchimedean semidefinite feasibility problems, of large scale, by means of stochastic game algorithms. In this paper, we show that the mean payoff of these games can be interpreted as a condition number for the corresponding nonarchimedean feasibility problems. This number measures how close a feasible instance is from being infeasible, and vice versa. We show that it coincides with the maximal radius of a ball in Hilbert's projective metric, that is included in the feasible set. The geometric interpretation of the condition number relies in particular on a duality theorem for tropical semidefinite feasibility programs. Then, we bound the complexity of the feasibility problem in terms of the condition number. We finally give explicit bounds for this condition number, in terms of the characteristics of the stochastic game. As a consequence, we show that the simplest algorithm to decide whether a stochastic mean payoff game is winning, namely value iteration, has a pseudopolynomial complexity when the number of random positions is fixed., Comment: 14 pages, 2 figures

Published
2018
Full Text
View/download PDF

12. k-maxitive fuzzy measures: a scalable approach to model interactions

Author

Serge Guillaume, Pilar Bulacio, Javier Murillo, Centro Franco Argentino de Ciencias de la Información y de Sistemas [Rosario] (CIFASIS), Universidad Nacional de Rosario [Santa Fe]-Consejo Nacional de Investigaciones Científicas y Técnicas [Buenos Aires] (CONICET), Information – Technologies – Analyse Environnementale – Procédés Agricoles (UMR ITAP), Institut national de recherche en sciences et technologies pour l'environnement et l'agriculture (IRSTEA)-Institut national d’études supérieures agronomiques de Montpellier (Montpellier SupAgro), Institut national d'enseignement supérieur pour l'agriculture, l'alimentation et l'environnement (Institut Agro)-Institut national d'enseignement supérieur pour l'agriculture, l'alimentation et l'environnement (Institut Agro), Consejo Nacional de Investigaciones Científicas y Técnicas [Buenos Aires] (CONICET)-Universidad Nacional de Rosario [Santa Fe], and Institut national d’études supérieures agronomiques de Montpellier (Montpellier SupAgro)-Institut national de recherche en sciences et technologies pour l'environnement et l'agriculture (IRSTEA)

Subjects
0209 industrial biotechnology, Theoretical computer science, Fuzzy classification, Computational complexity theory, Logic, 02 engineering and technology, Machine learning, computer.software_genre, Fuzzy logic, Measure (mathematics), CLASSIFICATION, MODELE, models, 020901 industrial engineering & automation, Artificial Intelligence, 0202 electrical engineering, electronic engineering, information engineering, Redundancy (engineering), Fuzzy number, MESURE, Mathematics, Fuzzy measure theory, business.industry, Heuristic, [SDE]Environmental Sciences, MATHEMATIQUES, 020201 artificial intelligence & image processing, Artificial intelligence, measurement, business, computer
Abstract

International audience; Fuzzy measures are powerful at modeling interactions between elements. Unfortunately, they use a number of coefficients that exponentially grows with the number of elements. Beyond the computational complexity, assigning a value to any coalition of a large set of elements does not make sense. k-order measures model interactions involving at most k elements. The number of coefficients to identify is reduced and their modeling capacity is preserved in real problems where the number of interacting elements is limited. In extreme situations of full redundancy or complementariness, it is mathematically proven that the complete fuzzy measure is both k-additive and k-maxitive. A learning algorithm to identify k-maxitive measures from labeled data is designed on the basis of HLMS (Heuristic Least Mean Squares). In a classification context, the study of synthetic data with partial redundancy or complementariness supports the idea that the difference between full and partial interaction is a matter of degree, not of kind. Dealing with two real world datasets, a comparison of the complete fuzzy measure and a k-maxitive one shows the number of interacting elements is limited and the k-maxitive measures yield the same characterization of interactions and a comparable classification accuracy.

Published
2017
Full Text
View/download PDF

13. A Formalization of Convex Polyhedra Based on the Simplex Method

Author

Xavier Allamigeon, Ricardo D. Katz, Allamigeon, Xavier, TROPICAL (TROPICAL), Centre de Mathématiques Appliquées - Ecole Polytechnique (CMAP), École polytechnique (X)-Centre National de la Recherche Scientifique (CNRS)-École polytechnique (X)-Centre National de la Recherche Scientifique (CNRS)-Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Centro Internacional Franco Argentino de Ciencias de la Información y de Sistemas (CIFASIS), Université Paul Cézanne - Aix-Marseille 3-Consejo Nacional de Investigaciones Científicas y Técnicas [Buenos Aires] (CONICET)-Universidad Nacional de Rosario [Santa Fe], Centro Franco Argentino de Ciencias de la Información y de Sistemas [Rosario] (CIFASIS), Consejo Nacional de Investigaciones Científicas y Técnicas [Buenos Aires] (CONICET)-Universidad Nacional de Rosario [Santa Fe], ANR-11-LABX-0056,LMH,LabEx Mathématique Hadamard(2011), and ANR-13-INSE-0003,MALTHY,Méthodes ALgèbriques pour la vérification de modèles Temporisés et HYbrides(2013)

Subjects
FOS: Computer and information sciences, Computer Science - Logic in Computer Science, Correctness, [INFO.INFO-LO] Computer Science [cs]/Logic in Computer Science [cs.LO], Linear programming, Computer science, Minkowski's theorem, 010103 numerical & computational mathematics, 0102 computer and information sciences, 02 engineering and technology, 01 natural sciences, Polyhedron, Simplex algorithm, Artificial Intelligence, TheoryofComputation_ANALYSISOFALGORITHMSANDPROBLEMCOMPLEXITY, Convex polytope, [MATH.MATH-CO]Mathematics [math]/Combinatorics [math.CO], FOS: Mathematics, 0202 electrical engineering, electronic engineering, information engineering, Mathematics::Metric Geometry, Mathematics - Combinatorics, 0101 mathematics, Simplex method, Mathematics - Optimization and Control, ComputingMilieux_MISCELLANEOUS, 010102 general mathematics, Proof assistant, Regular polygon, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], 020207 software engineering, [MATH.MATH-OC] Mathematics [math]/Optimization and Control [math.OC], Logic in Computer Science (cs.LO), Algebra, [MATH.MATH-CO] Mathematics [math]/Combinatorics [math.CO], TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, Computational Theory and Mathematics, Optimization and Control (math.OC), 010201 computation theory & mathematics, Combinatorics (math.CO), [MATH.MATH-OC]Mathematics [math]/Optimization and Control [math.OC], Farkas' lemma, Convex polyhedra, Formalization of mathematics, Software
Abstract

We present a formalization of convex polyhedra in the proof assistant Coq. The cornerstone of our work is a complete implementation of the simplex method, together with the proof of its correctness and termination. This allows us to define the basic predicates over polyhedra in an effective way (i.e., as programs), and relate them with the corresponding usual logical counterparts. To this end, we make an extensive use of the Boolean reflection methodology. The benefit of this approach is that we can easily derive the proof of several fundamental results on polyhedra, such as Farkas' Lemma, the duality theorem of linear programming, and Minkowski's Theorem., 18 pages, 2 figures, extended version

Published
2017
Full Text
View/download PDF

14. On the time discretization of stochastic optimal control problems: The dynamic programming approach

Author

Joseph Frédéric Bonnans, Francisco J. Silva, Justina Gianatti, Controle, Optimisation, modèles, Méthodes et Applications pour les Systèmes Dynamiques non linéaires (COMMANDS), Centre de Mathématiques Appliquées - Ecole Polytechnique (CMAP), École polytechnique (X)-Centre National de la Recherche Scientifique (CNRS)-École polytechnique (X)-Centre National de la Recherche Scientifique (CNRS)-Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Centro Franco Argentino de Ciencias de la Información y de Sistemas [Rosario] (CIFASIS), Consejo Nacional de Investigaciones Científicas y Técnicas [Buenos Aires] (CONICET)-Universidad Nacional de Rosario [Santa Fe], Mathématiques & Sécurité de l'information (XLIM-MATHIS), XLIM (XLIM), Université de Limoges (UNILIM)-Centre National de la Recherche Scientifique (CNRS)-Université de Limoges (UNILIM)-Centre National de la Recherche Scientifique (CNRS), and The first and second author thank the Laboratoire de Finance des Marchés de l’Energie for its support. The first and third authors thank the support from project iCODE :'Large-scale systems and Smart grids: distributed decision making and from the Gaspar Monge Program for Optimization and Operation Research (PGMO). The second author was also supported by Centro Internacional Franco Argentino de Ciencias de la Informacion y de Sistemas (CIFASI).

Subjects
0209 industrial biotechnology, Mathematical optimization, Control and Optimization, VALUE FUNCTION, Discretization, Matemáticas, Discrete Time Systems, Discrete-time stochastic process, 010103 numerical & computational mathematics, 02 engineering and technology, 01 natural sciences, purl.org/becyt/ford/1 [https], Dynamic Programming Principle, Discrete system, Value Function, 020901 industrial engineering & automation, DYNAMIC PROGRAMMING PRINCIPLE, Bellman equation, FEEDBACK CONTROL, 0101 mathematics, Stochastic Control, Primary: 93E20, 49L20, Secondary: 90C15, 93C55, Mathematics, Stochastic control, purl.org/becyt/ford/1.1 [https], DISCRETE TIME SYSTEMS, Matemática Aplicada, 16. Peace & justice, Stochastic programming, STOCHASTIC CONTROL, Dynamic programming, Computational Mathematics, Feedback Control, Discrete time and continuous time, Control and Systems Engineering, [MATH.MATH-OC]Mathematics [math]/Optimization and Control [math.OC], CIENCIAS NATURALES Y EXACTAS
Abstract

In this work, we consider the time discretization of stochastic optimal control problems. Under general assumptions on the data, we prove the convergence of the value functions associated with the discrete time problems to the value function of the original problem. Moreover, we prove that any sequence of optimal solutions of discrete problems is minimizing for the continuous one. As a consequence of the Dynamic Programming Principle for the discrete problems, the minimizing sequence can be taken in discrete time feedback form. Fil: Joseph Frédéric, Bonnans. Institut National de Recherche en Informatique et en Automatique; Francia. Centre National de la Recherche Scientifique; Francia. Université Paris-Saclay; Francia Fil: Gianatti, Justina. Consejo Nacional de Investigaciones Científicas y Técnicas. Centro Científico Tecnológico Conicet - Rosario. Centro Internacional Franco Argentino de Ciencias de la Información y de Sistemas. Universidad Nacional de Rosario. Centro Internacional Franco Argentino de Ciencias de la Información y de Sistemas; Argentina Fil: Silva, Francisco J.. Centre National de la Recherche Scientifique; Francia. Universite de Limoges; Francia

Published
2019
Full Text
View/download PDF

15. Tropicalization of facets of polytopes

Author

Xavier Allamigeon, Ricardo D. Katz, TROPICAL (TROPICAL), Centre de Mathématiques Appliquées - Ecole Polytechnique (CMAP), École polytechnique (X)-Centre National de la Recherche Scientifique (CNRS)-École polytechnique (X)-Centre National de la Recherche Scientifique (CNRS)-Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), École polytechnique (X)-Centre National de la Recherche Scientifique (CNRS), Centro Franco Argentino de Ciencias de la Información y de Sistemas [Rosario] (CIFASIS), Universidad Nacional de Rosario [Santa Fe]-Consejo Nacional de Investigaciones Científicas y Técnicas [Buenos Aires] (CONICET), The authors were partially supported by the PGMO program of EDF and Fondation Mathématique Jacques Hadamard. An important part of this work was done during a visit of Ricardo D. Katz to the Ecole Polytechnique, which was funded by Digitéo. Ricardo D. Katz was also partially supported by CONICET Grant PIP 11220110101026., and Consejo Nacional de Investigaciones Científicas y Técnicas [Buenos Aires] (CONICET)-Universidad Nacional de Rosario [Santa Fe]

Subjects
TROPICAL CONVEXITY, Matemáticas, 14T05, 52A01, FACET-DEFINING HALF-SPACES, Polytope, 0102 computer and information sciences, PUISEUX SERIES FIELD, 01 natural sciences, Puiseux series, Matemática Pura, Combinatorics, Lift (mathematics), purl.org/becyt/ford/1 [https], HAHN SERIES FIELD, Tropical convexity, [MATH.MATH-CO]Mathematics [math]/Combinatorics [math.CO], FOS: Mathematics, Discrete Mathematics and Combinatorics, Mathematics::Metric Geometry, Mathematics - Combinatorics, Puiseux series field, 0101 mathematics, Physics::Atmospheric and Oceanic Physics, Mathematics, Numerical Analysis, Algebra and Number Theory, Conjecture, Mathematics::Combinatorics, 010102 general mathematics, purl.org/becyt/ford/1.1 [https], external representations, 14T05 (Primary), 52A01 (Secondary), facet-defining half-spaces, 010201 computation theory & mathematics, EXTERNAL REPRESENTATIONS, polytopes, Combinatorics (math.CO), Geometry and Topology, General position, POLYTOPES, CIENCIAS NATURALES Y EXACTAS
Abstract

It is known that any tropical polytope is the image under the valuation map of ordinary polytopes over the Puiseux series field. The latter polytopes are called lifts of the tropical polytope. We prove that any pure tropical polytope is the intersection of the tropical half-spaces given by the images under the valuation map of the facet-defining half-spaces of a certain lift. We construct this lift explicitly, taking into account geometric properties of the given polytope. Moreover, when the generators of the tropical polytope are in general position, we prove that the above property is satisfied for any lift. This solves a conjecture of Develin and Yu., 18 pages, 6 figures; v2: major revision

Published
2014
Full Text
View/download PDF

16. Confluence via strong normalisation in an algebraic \lambda-calculus with rewriting

Author

Mauro Jaskelioff, Alejandro Díaz-Caro, Pablo Buiras, Departamento de Ciencias de la Computación [Rosario] (DCC), Facultad de Ciencias Exactas, Ingenieria y Agrimensura [Rosario] (FCEIA), Universidad Nacional de Rosario [Santa Fe]-Universidad Nacional de Rosario [Santa Fe], Calculs algorithmes programmes et preuves (CAPP), Laboratoire d'Informatique de Grenoble (LIG), Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Institut National Polytechnique de Grenoble (INPG)-Centre National de la Recherche Scientifique (CNRS)-Université Pierre Mendès France - Grenoble 2 (UPMF)-Université Joseph Fourier - Grenoble 1 (UJF)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Institut National Polytechnique de Grenoble (INPG)-Centre National de la Recherche Scientifique (CNRS)-Université Pierre Mendès France - Grenoble 2 (UPMF)-Université Joseph Fourier - Grenoble 1 (UJF), Centro Franco Argentino de Ciencias de la Información y de Sistemas [Rosario] (CIFASIS), Universidad Nacional de Rosario [Santa Fe]-Consejo Nacional de Investigaciones Científicas y Técnicas [Buenos Aires] (CONICET), grants from DIGITEO and Région Ile-de-France, CNRS-INS2I PEPS project QuAND, Simona Ronchi della Rocca and Elaine Pimentel, Université Pierre Mendès France - Grenoble 2 (UPMF)-Université Joseph Fourier - Grenoble 1 (UJF)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Institut National Polytechnique de Grenoble (INPG)-Centre National de la Recherche Scientifique (CNRS)-Université Pierre Mendès France - Grenoble 2 (UPMF)-Université Joseph Fourier - Grenoble 1 (UJF)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Institut National Polytechnique de Grenoble (INPG)-Centre National de la Recherche Scientifique (CNRS), and Consejo Nacional de Investigaciones Científicas y Técnicas [Buenos Aires] (CONICET)-Universidad Nacional de Rosario [Santa Fe]

Subjects
Computer Science - Logic in Computer Science, 0102 computer and information sciences, Type (model theory), 01 natural sciences, lcsh:QA75.5-76.95, Computer Science::Logic in Computer Science, ComputingMethodologies_SYMBOLICANDALGEBRAICMANIPULATION, 0101 mathematics, Algebraic number, Linear combination, Axiom, computer.programming_language, Mathematics, lcsh:Mathematics, 010102 general mathematics, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], 16. Peace & justice, lcsh:QA1-939, Algebra, TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, 010201 computation theory & mathematics, Confluence, TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, Linear algebra, Computer Science::Programming Languages, Rewriting, lcsh:Electronic computers. Computer science, Lambda calculus, computer
Abstract

The linear-algebraic lambda-calculus and the algebraic lambda-calculus are untyped lambda-calculi extended with arbitrary linear combinations of terms. The former presents the axioms of linear algebra in the form of a rewrite system, while the latter uses equalities. When given by rewrites, algebraic lambda-calculi are not confluent unless further restrictions are added. We provide a type system for the linear-algebraic lambda-calculus enforcing strong normalisation, which gives back confluence. The type system allows an abstract interpretation in System F., Comment: In Proceedings LSFA 2011, arXiv:1203.5423

Published
2011
Full Text
View/download PDF

Catalog

Books, media, physical & digital resources
See catalog results