scientific article; zbMATH DE number 7393562

zbMath1471.68052arXiv1309.1254MaRDI QIDQ4957786

Federico Aschieri

Publication date: 9 September 2021

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

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

Mathematics Subject Classification ID

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) Combinatory logic and lambda calculus (03B40)

Related Items (1)

On natural deduction in classical first-order logic: Curry-Howard correspondence, strong normalization and Herbrand's theorem

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A semantical proof of the strong normalization theorem for full propositional classical natural deduction
• Lectures on the Curry-Howard isomorphism
• A constructive valuation semantics for classical logic
• A symmetric lambda calculus for classical program extraction
• Nondeterministic extensions of untyped \(\lambda\)-calculus
• Probabilistic operational semantics for the lambda calculus
• Interactive Realizers
• Proofs of strong normalisation for second order classical natural deduction
• Interactive Realizability for Classical Peano Arithmetic with Skolem Axioms
• Non-determinism, Non-termination and the Strong Normalization of System T

This page was built for publication: