Non-determinism, non-termination and the strong normalization of System T

DOI10.1007/978-3-642-38946-7_5zbMATH Open1381.03020OpenAlexW48265284MaRDI QIDQ5300892FDOQ5300892

Authors Federico Aschieri, Margherita Zorzi 

Publication date 28 June 2013

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-38946-7_5

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05) Combinatory logic and lambda calculus (03B40)

Recommendations

• scientific article; zbMATH DE number 1499092
• New Computational Paradigms
• Strong normalisation for applied lambda calculi
• Short proofs of normalization for the simply-typed \(\lambda\)-calculus, permutative conversions and Gödel's \(\mathbf T\)
• Proving strong normalisation via non-deterministic translations into Klop's extended lambda-calculus

Cited in

(11)

• Strong normalisation for applied lambda calculi
• Title not available (Why is no real title available?)
• On natural deduction in classical first-order logic: Curry-Howard correspondence, strong normalization and Herbrand's theorem
• Quantum programming made easy
• QPCF: higher-order languages and quantum circuits
• Non-determinism in Gödel's system \(T\)
• On natural deduction for Herbrand constructive logics. I: Curry-Howard correspondence for Dummett's logic \(\mathsf {LC}\)
• Short proofs of normalization for the simply-typed \(\lambda\)-calculus, permutative conversions and Gödel's \(\mathbf T\)
• Continuous normalization for the lambda-calculus and Gödel's T
• Relational graph models at work
• \textsc{qPCF}: a language for quantum circuit computations

This page was built for publication: Non-determinism, non-termination and the strong normalization of System T

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5300892)