Pages that link to "Item:Q4382485"
From MaRDI portal
The following pages link to Proofs of strong normalisation for second order classical natural deduction (Q4382485):
Displaying 45 items.
- Böhm theorem and Böhm trees for the \(\varLambda \mu\)-calculus (Q428894) (← links)
- Deriving a Floyd-Hoare logic for non-local jumps from a formulæ-as-types notion of control (Q444460) (← links)
- Strong normalization results by translation (Q636353) (← links)
- A completeness result for the simply typed \(\lambda \mu \)-calculus (Q732057) (← 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)
- Termination of rewrite relations on \(\lambda\)-terms based on Girard's notion of reducibility (Q896904) (← links)
- Computational isomorphisms in classical logic (Q1398471) (← links)
- Non-strictly positive fixed points for classical natural deduction (Q1772778) (← links)
- An interpretation of \(\lambda \mu\)-calculus in \(\lambda\)-calculus. (Q1853149) (← links)
- Confluency and strong normalizability of call-by-value \(\lambda \mu\)-calculus (Q1853595) (← 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)
- Proof nets for classical logic (Q1982017) (← links)
- On the concurrent computational content of intermediate logics (Q1989344) (← links)
- Hypothetical logic of proofs (Q2254560) (← links)
- The differential \(\lambda \mu\)-calculus (Q2373711) (← links)
- A proof-theoretic foundation of abortive continuations (Q2464725) (← links)
- Strong normalization of classical natural deduction with disjunctions (Q2482841) (← links)
- Call-by-name reduction and cut-elimination in classical logic (Q2482842) (← links)
- Domain-Free<i>λµ</i>-Calculus (Q2729625) (← links)
- 2000 European Summer Meeting of the Association for Symbolic Logic. Logic Colloquium 2000 (Q2732529) (← links)
- A Context-based Approach to Proving Termination of Evaluation (Q2805157) (← links)
- Specifying Peirce's law in classical realizability (Q2973242) (← links)
- On Natural Deduction for Herbrand Constructive Logics I: Curry-Howard Correspondence for Dummett's Logic LC (Q2974784) (← links)
- A Classical Sequent Calculus with Dependent Types (Q2988668) (← links)
- Relating Computational Effects by ⊤ ⊤-Lifting (Q3012918) (← links)
- (Q3384877) (← links)
- Mixed Inductive/Coinductive Types and Strong Normalization (Q3498444) (← links)
- A Characterisation of Lambda Definability with Sums Via ⊤ ⊤-Closure Operators (Q3540185) (← links)
- Dual Calculus with Inductive and Coinductive Types (Q3636828) (← links)
- On the Values of Reducibility Candidates (Q3637200) (← links)
- An estimation for the lengths of reduction sequences of the $\lambda\mu\rho\theta$-calculus (Q4580321) (← links)
- (Q4957786) (← links)
- (Q4957787) (← links)
- (Q4957789) (← links)
- Programming and Proving with Classical Types (Q5055999) (← links)
- Implicative algebras: a new foundation for realizability and forcing (Q5139288) (← links)
- Relational Parametricity for Control Considered as a Computational Effect (Q5262944) (← links)
- Classical realizability and arithmetical formulæ (Q5360216) (← links)
- Monadic translation of classical sequent calculus (Q5410235) (← links)
- (Q5856422) (← links)
- Normalization in the simply typed -calculus (Q5889885) (← links)
- Strong normalizability of the non-deterministic catch/throw calculi (Q5958297) (← links)
- Adding Negation to Lambda Mu (Q6135761) (← links)
