The following pages link to (Q4255509):
Displaying 50 items.
- On natural deduction in classical first-order logic: Curry-Howard correspondence, strong normalization and Herbrand's theorem (Q265002) (← links)
- Applicative bisimilarities for call-by-name and call-by-value \(\lambda\mu\)-calculus (Q283739) (← links)
- Natural deduction for the Sheffer stroke and Peirce's arrow (and any other truth-functional connective) (Q288247) (← links)
- Semantic types and approximation for Featherweight Java (Q387991) (← links)
- Böhm theorem and Böhm trees for the \(\varLambda \mu\)-calculus (Q428894) (← links)
- Compositional Z: confluence proofs for permutative conversion (Q514511) (← links)
- Preface to the special volume (Q534064) (← links)
- Polarized and focalized linear and classical proofs (Q556824) (← links)
- Strong normalisation in the \(\pi\)-calculus (Q598201) (← links)
- Strong normalization results by translation (Q636353) (← links)
- Kripke models for classical logic (Q636371) (← links)
- Completeness and partial soundness results for intersection and union typing for \(\overline{\lambda}\mu\tilde{\mu}\) (Q636376) (← links)
- Type checking and typability in domain-free lambda calculi (Q655411) (← links)
- Pedagogical second-order \(\lambda \)-calculus (Q732007) (← links)
- A completeness result for the simply typed \(\lambda \mu \)-calculus (Q732057) (← links)
- The \(\lambda \)-calculus and the unity of structural proof theory (Q733755) (← links)
- A semantical proof of the strong normalization theorem for full propositional classical natural deduction (Q818927) (← links)
- Strong normalization proofs by CPS-translations (Q845711) (← links)
- Categorical proof theory of classical propositional calculus (Q860833) (← links)
- Resource operators for \(\lambda\)-calculus (Q876041) (← links)
- Combining algebraic effects with continuations (Q879352) (← links)
- A syntactic correspondence between context-sensitive calculi and abstract machines (Q879356) (← links)
- Reduction rules for intuitionistic \(\lambda\rho\)-calculus (Q897480) (← links)
- Characterizing strong normalization in the Curien-Herbelin symmetric lambda calculus: extending the Coppo-Dezani heritage (Q930871) (← links)
- CERES: An analysis of Fürstenberg's proof of the infinity of primes (Q944367) (← links)
- A type-theoretic foundation of delimited continuations (Q968364) (← links)
- Counting proofs in propositional logic (Q1014285) (← links)
- CPS-translation as adjoint (Q1044830) (← links)
- Full intuitionistic linear logic (Q1314646) (← links)
- Classical logic, storage operators and second-order lambda-calculus (Q1326769) (← links)
- A general storage theorem for integers in call-by-name \(\lambda\)- calculus (Q1329740) (← links)
- Intuitionistic and classical natural deduction systems with the catch and the throw rules (Q1392143) (← links)
- Computational isomorphisms in classical logic (Q1398471) (← links)
- On the intuitionistic force of classical search (Q1575923) (← links)
- Search algorithms in type theory (Q1575934) (← links)
- Proof-search in type-theoretic languages: An introduction (Q1575935) (← links)
- The Cooper storage idiom (Q1711505) (← links)
- Classical natural deduction for S4 modal logic (Q1758660) (← links)
- The computational content of arithmetical proofs (Q1762353) (← links)
- Uniform Heyting arithmetic (Q1772775) (← links)
- Non-strictly positive fixed points for classical natural deduction (Q1772778) (← links)
- About classical logic and imperative programming (Q1817076) (← links)
- An interpretation of \(\lambda \mu\)-calculus in \(\lambda\)-calculus. (Q1853149) (← links)
- Polarized proof-nets and \(\lambda \mu\)-calculus (Q1853586) (← links)
- Confluency and strong normalizability of call-by-value \(\lambda \mu\)-calculus (Q1853595) (← links)
- Structural cut elimination. I: Intuitionistic and classical logic (Q1854335) (← links)
- Church-Rosser property of a simple reduction for full first-order classical natural deduction (Q1861541) (← links)
- Strong normalization of the second-order symmetric \(\lambda \mu\)-calculus (Q1881230) (← links)
- Getting results from programs extracted from classical proofs (Q1882897) (← links)
- Dependent choice, `quote' and the clock (Q1884884) (← links)
