A symmetric lambda calculus for classical program extraction
From MaRDI portal
Publication:1917084
DOI10.1006/inco.1996.0025zbMath0853.68159OpenAlexW2177357765MaRDI QIDQ1917084
Franco Barbanera, Stefano Berardi
Publication date: 5 January 1997
Published in: Information and Computation (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1006/inco.1996.0025
Related Items
Classical Logic with Mendler Induction, Strong normalization of the second-order symmetric \(\lambda \mu\)-calculus, Unnamed Item, Call-by-Value Is Dual to Call-by-Name, Extended, Classical realizability and arithmetical formulæ, Böhm theorem and Böhm trees for the \(\varLambda \mu\)-calculus, Computation with classical sequents, Specifying Peirce's law in classical realizability, Unnamed Item, A Classical Sequent Calculus with Dependent Types, Characterizing strong normalization in the Curien-Herbelin symmetric lambda calculus: extending the Coppo-Dezani heritage, A new deconstructive logic: linear logic, The Church-Rosser property in symmetric combinatory logic, 2002–2003 Winter Meeting of the Association for Symbolic Logic, 2002 Annual Conference of the Australasian Association for Logic, Classical \(F_{\omega}\), orthogonality and symmetric candidates, On categorical models of classical logic and the Geometry of Interaction, An estimation for the lengths of reduction sequences of the $\lambda\mu\rho\theta$-calculus, Investigations on the dual calculus, Dual Calculus with Inductive and Coinductive Types, Social processes, program verification and all that, Semantics for dual and symmetric combinatory calculi, Intersection Types for the Resource Control Lambda Calculi, Unnamed Item, Search algorithms in type theory
