become an editor
the entire directory
only in Formulae-as-Types_Correspondence/Classical_Logic
Logic and Foundations
Combinatory Logic and Lambda Calculus
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.
" search on:
to edit this category.
Copyright © 1998-2015 AOL Inc.
Visit our sister sites
Last update: June 26, 2012 at 12:54:03 UTC -