Sciweavers

LISP
2006
76views more  LISP 2006»
13 years 3 months ago
Semantics of roundoff error propagation in finite precision calculations
We introduce a concrete semantics for floating-point operations which describes the propagation of roundoff errors throughout a calculation. This semantics is used to assert the co...
Matthieu Martel
LISP
2006
91views more  LISP 2006»
13 years 3 months ago
Polymorphic typed defunctionalization and concretization
Abstract. Defunctionalization is a program transformation that eliminates functions as first-class values. We show that defunctionalization can be viewed as a type-preserving trans...
François Pottier, Nadji Gauthier
LISP
2006
77views more  LISP 2006»
13 years 3 months ago
Expressing combinatory reduction systems derivations in the rewriting calculus
The last few years have seen the development of the rewriting calculus (also called rho-calculus or -calculus) that uniformly integrates first-order term rewriting and the -calculu...
Clara Bertolissi, Horatiu Cirstea, Claude Kirchner
LISP
2006
160views more  LISP 2006»
13 years 3 months ago
Formal compiler construction in a logical framework
The task of designing and implementing a compiler can be a difficult and error-prone process. In this paper, we present a new approach based on the igher-order abstract syntax and ...
Jason Hickey, Aleksey Nogin
LISP
2006
117views more  LISP 2006»
13 years 3 months ago
About permutation algebras, (pre)sheaves and named sets
In this paper we survey some well-known approaches proposed as general models for calculi dealing with names (like for example process calculi with name-passing). We focus on (pre)...
Fabio Gadducci, Marino Miculan, Ugo Montanari
LISP
2006
105views more  LISP 2006»
13 years 3 months ago
Call-by-push-value: Decomposing call-by-value and call-by-name
We present the call-by-push-value (CBPV) calculus, which decomposes the typed call-by-value (CBV) and typed call-by-name (CBN) paradigms into fine-grain primitives. On the operatio...
Paul Blain Levy