We define and study a term calculus implementing higher-order node replication. It is used to specify two different (weak) evaluation strategies: call-by-name and fully lazy call-by-need, that are shown to be observationally equivalent by using type theoretical technical tools.

Abstract We define and study a term calculus implementing higher-order node replication. It is used to specify two different (weak) evaluation strategies: call-by-name and fully lazy call-by-need, that are shown to be observationally equivalent by using type theoretical technical tools.

We investigate a new computational interpretation for an intuitionistic focused sequent calculus which is compatible with a resource aware semantics. For that, we associate to Herbelin's syntax a type system based on non-idempotent intersection types, together with a set of reduction rules – inspired from thesubstitution at a distanceparadigm – that preserves (and decreases the size of) typing derivations. The non-idempotent approach allows us to use very simple combinatorial arguments, only based on this measure decreasingness, to characterizelinear-headandstronglynormalizing terms by means of typability. For the sake of completeness, we also study typability (and the corresponding strong normalization characterization) in the calculus obtained from the former one by projecting the explicit cuts.