1. Franco Barbanera & Stefano Berardi (1996). A Constructive Valuation Semantics for Classical Logic. Notre Dame Journal of Formal Logic 37 (3):462-482.
    This paper presents a constructive interpretation for the proofs in classical logic of $\Sigma^0_1$ -sentences and for a witness extraction procedure based on Prawitz's reduction rules.
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  2. Franco Barbanera & Stefano Berardi (1995). A Strong Normalization Result for Classical Logic. Annals of Pure and Applied Logic 76 (2):99-116.
    In this paper we give a strong normalization proof for a set of reduction rules for classical logic. These reductions, more general than the ones usually considered in literature, are inspired to the reductions of Felleisen's lambda calculus with continuations.
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  3. Franco Barbanera & Simone Martini (1994). Proof-Functional Connectives and Realizability. Archive for Mathematical Logic 33 (3):189-211.
    The meaning of a formula built out of proof-functional connectives depends in an essential way upon the intensional aspect of the proofs of the component subformulas. We study three such connectives, strong equivalence (where the two directions of the equivalence are established by mutually inverse maps), strong conjunction (where the two components of the conjunction are established by the same proof) and relevant implication (where the implication is established by an identity map). For each of these connectives we give a (...)
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation