scientific article; zbMATH DE number 7393562

MaRDI QIDQ4957786zbMATH OpenFDO

Authors Federico Aschieri

Publication date 9 September 2021

Full work available at URL https://arxiv.org/abs/1309.1254, http://eptcs.web.cse.unsw.edu.au/paper.cgi?COS2013.1

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Logic in computer science (03B70) Cut-elimination and normal-form theorems (03F05) First-order arithmetic and fragments (03F30) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• Realizability and strong normalization for a Curry-Howard interpretation of HA + EM1
• scientific article; zbMATH DE number 4055611
• A simple proof of the undecidability of strong normalisation
• Short Proofs of Strong Normalization
• scientific article; zbMATH DE number 7599997
• On strong normalities
• Strong normalization theorems for quantized -calculi
• A proof of strong normalisation using domain theory
• Strong normalization proofs by CPS-translations
• scientific article; zbMATH DE number 1508933

Cites work

• A constructive valuation semantics for classical logic
• A new use of Friedman's translation: interactive realizability
• A semantical proof of the strong normalization theorem for full propositional classical natural deduction
• A symmetric lambda calculus for classical program extraction
• scientific article; zbMATH DE number 1722654 (Why is no real title available?)
• scientific article; zbMATH DE number 2185662 (Why is no real title available?)
• scientific article; zbMATH DE number 5851813 (Why is no real title available?)
• scientific article; zbMATH DE number 42059 (Why is no real title available?)
• scientific article; zbMATH DE number 46869 (Why is no real title available?)
• scientific article; zbMATH DE number 1215498 (Why is no real title available?)
• scientific article; zbMATH DE number 512771 (Why is no real title available?)
• scientific article; zbMATH DE number 517083 (Why is no real title available?)
• scientific article; zbMATH DE number 1420833 (Why is no real title available?)
• scientific article; zbMATH DE number 3275554 (Why is no real title available?)
• scientific article; zbMATH DE number 3358455 (Why is no real title available?)
• Interactive realizability for classical Peano arithmetic with Skolem axioms
• Interactive realizers: a new approach to program extraction from nonconstructive proofs
• Lectures on the Curry-Howard isomorphism
• Non-determinism, non-termination and the strong normalization of System T
• Nondeterministic extensions of untyped \(\lambda\)-calculus
• Probabilistic operational semantics for the lambda calculus
• Proofs of strong normalisation for second order classical natural deduction
• Realizability and strong normalization for a Curry-Howard interpretation of HA + EM1

Cited in

(3)

• On natural deduction in classical first-order logic: Curry-Howard correspondence, strong normalization and Herbrand's theorem
• Realizability and strong normalization for a Curry-Howard interpretation of HA + EM1
• On natural deduction for Herbrand constructive logics. II: Curry-Howard correspondence for Markov's principle in first-order logic and arithmetic

This page was built for publication:

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