Sciweavers

LISP
2006
76views more  LISP 2006»
14 years 12 days 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»
14 years 12 days 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»
14 years 12 days 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»
14 years 12 days 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»
14 years 12 days 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»
14 years 12 days 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