Publication:4281464
From MaRDI portal
zbMath0788.68016MaRDI QIDQ4281464
Stefano Berardi, Franco Barbanera
Publication date: 10 March 1994
68Q45: Formal languages and automata
68N15: Theory of programming languages
03F05: Cut-elimination and normal-form theorems
03F30: First-order arithmetic and fragments
03B40: Combinatory logic and lambda calculus
Related Items
Refined program extraction from classical proofs, Strong normalizability of the non-deterministic catch/throw calculi, Deriving a Floyd-Hoare logic for non-local jumps from a formulæ-as-types notion of control, A type-theoretic foundation of delimited continuations, Search algorithms in type theory, Uniform Heyting arithmetic, A strong normalization result for classical logic, A proof-theoretic foundation of abortive continuations, Domain-Freeλµ-Calculus, Classical truth in higher types