scientific article
From MaRDI portal
Publication:3075442
zbMath1206.03017MaRDI QIDQ3075442
Publication date: 15 February 2011
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Curry-Howard isomorphismlambda-calculusclassical realizabilityaxiom of dependent choiceproof-program correspondence
Functional programming and lambda calculus (68N18) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Combinatory logic and lambda calculus (03B40)
Related Items (24)
On natural deduction in classical first-order logic: Curry-Howard correspondence, strong normalization and Herbrand's theorem ⋮ Quantum Control in the Unitary Sphere: Lambda-S1 and its Categorical Model ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Realizability for Peano arithmetic with winning conditions in HON games ⋮ Interaction graphs: graphings ⋮ Stateful Realizers for Nonstandard Analysis ⋮ Realizability algebras III: some examples ⋮ A correspondence between maximal abelian sub-algebras and linear logic fragments ⋮ Constructive forcing, CPS translations and witness extraction in Interactive realizability ⋮ Unnamed Item ⋮ Realizability in ordered combinatory algebras with adjunction ⋮ A Classical Sequent Calculus with Dependent Types ⋮ Implicative algebras: a new foundation for realizability and forcing ⋮ Mathematical logic: proof theory, constructive mathematics. Abstracts from the workshop held November 5--11, 2017 ⋮ Verificationism and Classical Realizability ⋮ Computational Interpretations of Classical Reasoning: From the Epsilon Calculus to Stateful Programs ⋮ Classical realizability in the CPS target language ⋮ Codensity Lifting of Monads and its Dual ⋮ Unnamed Item ⋮ Unnamed Item ⋮ GAME SEMANTICS AND THE GEOMETRY OF BACKTRACKING: A NEW COMPLEXITY ANALYSIS OF INTERACTION ⋮ Unnamed Item ⋮ Realizability models for a linear dependent PCF
This page was built for publication:
