scientific article; zbMATH DE number 7393562

zbMATH Open1471.68052arXiv1309.1254MaRDI QIDQ4957786FDOQ4957786

Authors: Federico Aschieri 

Publication date: 9 September 2021

Full work available at URL: https://arxiv.org/abs/1309.1254

Title of this publication is not available (Why is that?)

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 \(\lambda \)-calculi
• A proof of strong normalisation using domain theory
• Strong normalization proofs by CPS-translations
• scientific article; zbMATH DE number 1508933

Mathematics Subject Classification ID

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

Cites Work

• Nondeterministic extensions of untyped \(\lambda\)-calculus
• Title not available (Why is that?)
• Probabilistic operational semantics for the lambda calculus
• Interactive realizers: a new approach to program extraction from nonconstructive proofs
• Realizability and strong normalization for a Curry-Howard interpretation of HA + EM1
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Interactive realizability for classical Peano arithmetic with Skolem axioms
• A new use of Friedman's translation: interactive realizability
• Non-determinism, non-termination and the strong normalization of System T
• Title not available (Why is that?)
• Title not available (Why is that?)
• Lectures on the Curry-Howard isomorphism
• Title not available (Why is that?)
• Title not available (Why is that?)
• A symmetric lambda calculus for classical program extraction
• Proofs of strong normalisation for second order classical natural deduction
• Title not available (Why is that?)
• Title not available (Why is that?)
• A semantical proof of the strong normalization theorem for full propositional classical natural deduction
• A constructive valuation semantics for classical logic
• Title not available (Why is that?)

Cited In (2)

• 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

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)