This site uses cookies to deliver our services and to ensure you get the best experience. By continuing to use this site, you consent to our use of cookies and acknowledge that you have read and understand our Privacy Policy, Cookie Policy, and Terms
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...
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...
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
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 ...
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)...
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...