Science Math Logic and Foundations Computational Logic Combinatory Logic and Lambda Calculus Formulae-as-Types Correspondence
Classical Logic

7

The formulae-as-types correspondence is normally understood as giving
a constructive interpretation for a logic, whilst classical logic is
normally understood as resisting an interpreatation. Thus results
that show that classical logic admits a formulae-as-types
correspondence have provoked a lot of interest in the research community.

### Sites 7

Computational Content of Classical Logic (1996)

Lecture notes from a research seminar series by Thierry Coquand covering double-negation translations, game semantics of classical logic and point-free topology.

Computational Isomorphisms in Classical Logic

Article by V. Danos, J. B. Joinet and H. Schellinx examining the categorical semantics of classical logic from a perspective inspired by linear logic.

CPS Translations and Applications: the Cube and Beyond (1996)

Article by G. Barthe, J. Hatcliff, and M.H. SÃ¸rensen which presents a CPS translation to Barenderegt's `cube' of pure type systems, and applies this to provide a formulae-as-types correspondence for higher-order classical predicate logic.

A Curry-Howard Foundation for Functional Computation with Control (1997)

Article by C.-H. L. Ong and C. A. Stewart which presents a call-by-name variant of Parigot's lambda-mu calculus. The calculus is proposed as a foundation for first-class continuations and statically scoped exceptions in functional programming languages.

A Notion of Classical Pure Type System (1997)

Article by Gilles Barthes.

On the computational content of the Axiom of Choice (1995)

Article by S. Berardi, M. Bezem and T. Coquand presenting a possible computational content of the negative translation of classical analysis with the Axiom of Choice.

A Semantic View of Classical Proofs (1996)

Article by C.-H. Luke Ong presenting the semantics of classical proof theory from three perspectives: a formulae-as-types characterisation in a variant of Parigot's lambda-mu calculus, a denotational characterisation in game semantics, and a categorical semantics as a fibred CCC.

Last update:

June 26, 2012 at 12:54:03 UTC
Copyright © 1998-2016 AOL Inc.

Built by CMBuild