scientific article; zbMATH DE number 7393562
From MaRDI portal
Publication:4957786
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
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)
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)