ICFP

2012

ACM

12 years 8 days ago
2012

ACM

Continuing a line of work by Abramsky (1994), by Bellin and Scott (1994), and by Caires and Pfenning (2010), among others, this paper presents CP, a calculus in which propositions...

TOCL

2012

12 years 8 days ago
2012

racting these leads us to introduce the notion of a path object category. This is a relatively simple axiomatic framework, which is nonetheless suﬃciently strong to allow the con...

LICS

2012

IEEE

12 years 8 days ago
2012

IEEE

—We propose a mathematical framework for step indexed realizability semantics of a call-by-value polymorphic lambda calculus with recursion, existential types and recursive types...

LOGCOM

2010

13 years 8 months ago
2010

The aim of this paper is double. From one side we survey the knowledge we have acquired these last ten years about the lattice of all λ-theories (= equational extensions of untype...

MSCS

2000

13 years 9 months ago
2000

This paper introduces a Hilbert system for lambda calculus called sequent combinators. Sequent combinators address many of the problems of Hilbert systems, which have led to the m...

CORR

2008

Springer

13 years 10 months ago
2008

Springer

This is a set of lecture notes that developed out of courses on the lambda calculus that I taught at the University of Ottawa in 2001 and at Dalhousie University in 2007. Topics c...

APLAS

2001

ACM

14 years 1 months ago
2001

ACM

Abstract. We propose a semantic and syntactic framework for modelling linearly used effects, by giving the monadic transforms of the computational lambda calculus (considered as th...

ASIAN

2006

Springer

14 years 1 months ago
2006

Springer

Interesting properties of programs can be expressed using contextual equivalence. The latter is difficult to prove directly, hence (pre-)logical relations are often used as a tool ...

RTA

2010

Springer

14 years 1 months ago
2010

Springer

This paper shows the equivalence of applicative similarity and contextual approximation, and hence also of bisimilarity and contextual equivalence, in the deterministic call-by-nee...

PEPM

1997

ACM

14 years 2 months ago
1997

ACM

Recently, Olivier Danvy introduced a new, simple method for implementing powerful partial evaluators, namely typedirected partial evaluation 9 . He introduced a partial evaluator ...