Alexandria

Resource-safe Systems Programming with Embedded Domain Specific Languages

Edwin Brady Kevin Hammond (2011)

We introduce a new overloading notation that facilitates programming, modularity and reuse in Embedded Domain Specific Languages (EDSLs), and use it to reason about safe resource usage and state management. We separate the structural language constructs from our primitive operations, and show how precisely-typed functions can be lifted into the EDSL. In this way, we implement a generic framework for constructing state-aware EDSLs for systems programming.

3 commentaires

Lire maintenant ?

Computational Geometry

Michael Shamos (1978)

Cette thèse de 1978 a fait naître un domaine : la géométrie algorithmique. L’auteur a étudié attentivement la géométrie et l’algorithmique, et sa thèse est remplie de questions d’entretiens^W^W méthodes encore utilisées aujourd’hui pour un bon nombre de problème géométriques :

• test de convexité ;
• enveloppe convexe ;
• diamètre d’un polygone ;
• intersections ;
• plus proches voisins ;
• diagrammes de Voronoï.

Pour ne citer qu’un domaine d’application, le jeu vidéo utilise énormément les intersections et les plus proches voisins.

L’algorithme utilisé pour déterminer le diamètre d’un polygone (la distance maximum entre deux points) est assez élégant et mérite d’être connu. Il s’exécute en O(n) une fois qu’on a l’enveloppe convexe (qui peut aussi se faire en O(n) suivant les préconditions). On l’appelle l’algorithme des "rotating calipers" (littéralement pieds à coulisse rotatifs) et il a ensuite été généralisé à une myriade d'autres problèmes.

Un commentaire

Lire maintenant ?

How efficient is speech?

R.J.J.H. van Son Louis C.W. Pols (2003)

Speech is considered an efficient communication channel. This implies that the organization of utterances is such that more speaking effort is directed towards important parts than towards redundant parts. Based on a model of incremental word recognition, the importance of a segment is defined as its contribution to word-disambiguation. This importance is measured as the segmental information content, in bits. On a labeled Dutch speech corpus it is then shown that crucial aspects of the information structure of utterances partition the segmental information content and explain 90% of the variance. Two measures of acoustical reduction, duration and spectral center of gravity, are correlated with the segmental information content in such a way that more important phonemes are less reduced. It is concluded that the organization of reduction according to conventional information structure does indeed increase efficiency.

Un commentaire

Lire maintenant ?

Relaxing the Value Restriction

Jacques Garrigue (2004)

Restricting polymorphism to values is now the standard way to obtain soundness in ML-like programming languages with imperative features. While this solution has undeniable advantages over previous approaches, it forbids polymorphism in many cases where it would be sound. We use a subtyping based approach to recover part of this lost polymorphism, without changing the type algebra itself, and this has significant applications.

Un commentaire

Lire maintenant ?

Formal Proof -- The Four-Colors Theorem

Georges Gonthier (2008)

In 2005, we achieved the formalization of the entire proof of the Four-Color Theorem, not just its code. While we tackled this project mainly to explore the capabilities of a modern formal proof system —at first, to benchmark speed— we were pleasantly surprised to uncover new and rather elegant nuggets of mathematics in the process. In hindsight this might have been expected: to produce a formal proof one must make explicit every single logical step of a proof; Perhaps this is the most promising aspect of formal proof: it is not merely a method to make absolutely sure we have not made a mistake in a proof, but also a tool that shows us and compels us to understand why a proof works.

In this article, the next two sections contain background material, describing the original proof and the Coq formal system we used. The following two sections describe the sometimes new mathematics involved in the formalization. Then the next two sections go into some detail into the two main parts of the formal proof: reducibility and unavoidability. The Coq code (available at the same address) is the ultimate reference for the intrepid, who should bone up on Coq beforehand.

Commenter

Lire maintenant ?