Publication

Miniboxing: Improving the Speed to Code Size Tradeoff in Parametric Polymorphism Translations

Concepts associés (43)

Graph Chatbot

Chattez avec Graph Search

Posez n’importe quelle question sur les cours, conférences, exercices, recherches, actualités, etc. de l’EPFL ou essayez les exemples de questions ci-dessous.

AVERTISSEMENT : Le chatbot Graph n'est pas programmé pour fournir des réponses explicites ou catégoriques à vos questions. Il transforme plutôt vos questions en demandes API qui sont distribuées aux différents services informatiques officiellement administrés par l'EPFL. Son but est uniquement de collecter et de recommander des références pertinentes à des contenus que vous pouvez explorer pour vous aider à répondre à vos questions.

Connectez-vous pour utiliser Chat avec Graph Search

Bounded quantification

In type theory, bounded quantification (also bounded polymorphism or constrained genericity) refers to universal or existential quantifiers which are restricted ("bounded") to range only over the subtypes of a particular type. Bounded quantification is an interaction of parametric polymorphism with subtyping. Bounded quantification has traditionally been studied in the functional setting of System F

Double-precision floating-point format

Double-precision floating-point format (sometimes called FP64 or float64) is a floating-point number format, usually occupying 64 bits in computer memory; it represents a wide dynamic range of numeric values by using a floating radix point. Floating point is used to represent fractional values, or when a wider range is needed than is provided by fixed point (of the same bit width), even if at the cost of precision. Double precision may be chosen when the range or precision of single precision would be insufficient.

OCaml

OCaml, anciennement connu sous le nom d'Objective Caml, est l'implémentation la plus avancée du langage de programmation Caml, créé par Xavier Leroy, Jérôme Vouillon, , Didier Rémy et leurs collaborateurs en 1996. Ce langage, de la famille des langages ML, est un projet open source dirigé et maintenu essentiellement par l'Inria. OCaml est le successeur de Caml Light, auquel il a ajouté entre autres une couche de programmation objet.

Réification

La réification (du latin « chose ») consiste à réifier, c'est-à-dire à donner les caractéristiques ou transformer en chose ce qui ne l'est pas, tel que considérer une personne comme un objet ou bien une idée abstraite comme un élément concret, ou à leur donner un caractère statique ou figé. Dans l'usage ordinaire du langage, il est normal de réifier des idées et la réification sera comprise comme telle.

Bfloat16 floating-point format

The bfloat16 (brain floating point) floating-point format is a computer number format occupying 16 bits in computer memory; it represents a wide dynamic range of numeric values by using a floating radix point. This format is a truncated (16-bit) version of the 32-bit IEEE 754 single-precision floating-point format (binary32) with the intent of accelerating machine learning and near-sensor computing. It preserves the approximate dynamic range of 32-bit floating-point numbers by retaining 8 exponent bits, but supports only an 8-bit precision rather than the 24-bit significand of the binary32 format.

Top type

In mathematical logic and computer science, some type theories and type systems include a top type that is commonly denoted with top or the symbol ⊤. The top type is sometimes called also universal type, or universal supertype as all other types in the type system of interest are subtypes of it, and in most cases, it contains every possible object of the type system. It is in contrast with the bottom type, or the universal subtype, which every other type is supertype of and it is often that the type contains no members at all.

Entier (informatique)

En informatique, un entier est un type de donnée qui représente un sous-ensemble fini de nombres entiers relatifs. On utilise aussi le terme type de données entières (integral type data). Un type de donnée est la nature des valeurs que peut prendre une donnée. Certains traitements comme le recensement des États-Unis ont d'abord été effectués en utilisant une représentation décimale à l'aide de cartes perforées. Le système décimal utilise dix chiffres (0, 1, 2, 3, 4, 5, 6, 7, 8, 9) et où leur position correspond à une puissance de 10 (1, 10, 100, 1000, etc.

Programming language implementation

In computer programming, a programming language implementation is a system for executing computer programs. There are two general approaches to programming language implementation: Interpretation: The program is read as input by an interpreter, which performs the actions written in the program. Compilation: The program is read by a compiler, which translates it into some other language, such as bytecode or machine code. The translated code may either be directly executed by hardware, or serve as input to another interpreter or another compiler.

Implémentation de référence

Dans le processus de développement de logiciel, une implémentation de référence (aussi appelé, moins fréquemment, exemple de mise en œuvre ou modèle d'implémentation) est la norme à partir de laquelle toutes les autres implémentations et les autres personnalisations sont dérivées. Une amélioration à une implémentation de référence ne reflète pas un changement de la spécification sous-jacente. À l'inverse, l'échec d'une de la mise en œuvre d'une implémentation de référence peut s'avérer être la preuve que le cahier des charges n'est pas adapté et qu'il nécessite une amélioration.

Kind (type theory)

In the area of mathematical logic and computer science known as type theory, a kind is the type of a type constructor or, less commonly, the type of a higher-order type operator. A kind system is essentially a simply typed lambda calculus "one level up", endowed with a primitive type, denoted and called "type", which is the kind of any data type which does not need any type parameters. A kind is sometimes confusingly described as the "type of a (data) type", but it is actually more of an arity specifier.