A reformulation of Parigot's lambda-mu-calculus will be presented, together with applications to proof theory (natural deduction for classical logic, Curry-Howard interpretation of sequent calculus) and to the theory of programming languages (call-by-value lambda-calculus, foundations for let-expressions).