Typage polymorphe d'un langage algorithmique

Abstract : The polymorphic type discipline, as in the ML language, fits well within purely applicative languages, but does not extend naturally to the main feature of algorithmic languages: in-place update of data structures. Similar typing difficulties arise with other extensions of applicative languages: logical variables, communication channels, continuation handling. This work studies (in the setting of relational semantics) two new approaches to the polymorphic typing of these non-applicative features. The first one relies on a restriction of generalization over types (the notion of dangerous variables), and on a refined typing of functional values (closure typing). The resulting type system is compatible with the ML core language, and is the most expressive type systems for ML with imperative features proposed so far. The second approach relies on switching to ``by-name'' semantics for the constructs of polymorphism, instead of the usual ``by-value'' semantics. The resulting language differs from ML, but lends itself easily to polymorphic typing. Both approaches smoothly integrate non-applicative features and polymorphic typing.
Document type :
Theses
Complete list of metadatas

Cited literature [107 references]  Display  Hide  Download

https://hal.inria.fr/tel-01499951
Contributor : Xavier Leroy <>
Submitted on : Saturday, April 1, 2017 - 6:11:52 PM
Last modification on : Thursday, April 26, 2018 - 10:28:51 AM
Long-term archiving on : Sunday, July 2, 2017 - 12:51:47 PM

Identifiers

  • HAL Id : tel-01499951, version 1

Collections

Relations

  • has version inria-00077018 - English translation / Traduction en anglais

Citation

Xavier Leroy. Typage polymorphe d'un langage algorithmique. Langage de programmation [cs.PL]. Université Paris 7, 1992. Français. ⟨tel-01499951⟩

Share

Metrics

Record views

380

Files downloads

208