Realizability Interpretation and Normalization of Typed Call-by-Need λ-calculus With Control

Autor: Étienne Miquey, Hugo Herbelin
Přispěvatelé: Gallinette : vers une nouvelle génération d'assistant à la preuve (GALLINETTE), Inria Rennes – Bretagne Atlantique, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire des Sciences du Numérique de Nantes (LS2N), IMT Atlantique Bretagne-Pays de la Loire (IMT Atlantique), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT)-Université de Nantes - UFR des Sciences et des Techniques (UN UFR ST), Université de Nantes (UN)-Université de Nantes (UN)-École Centrale de Nantes (ECN)-Centre National de la Recherche Scientifique (CNRS)-IMT Atlantique Bretagne-Pays de la Loire (IMT Atlantique), Université de Nantes (UN)-Université de Nantes (UN)-École Centrale de Nantes (ECN)-Centre National de la Recherche Scientifique (CNRS), Design, study and implementation of languages for proofs and programs (PI.R2), Université Paris Diderot - Paris 7 (UPD7)-Centre National de la Recherche Scientifique (CNRS)-Institut de Recherche en Informatique Fondamentale (IRIF (UMR_8243)), Université Paris Diderot - Paris 7 (UPD7)-Centre National de la Recherche Scientifique (CNRS)-Université Paris Diderot - Paris 7 (UPD7)-Centre National de la Recherche Scientifique (CNRS)-Inria de Paris, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Christel Baier, Ugo Dal Lago, Université de Nantes - Faculté des Sciences et des Techniques, Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT)-Université de Nantes - Faculté des Sciences et des Techniques, Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT), Gallinette : vers une nouvelle génération d'assistant à la preuve (LS2N - équipe GALLINETTE), Université de Nantes - UFR des Sciences et des Techniques (UN UFR ST), Université de Nantes (UN)-Université de Nantes (UN)-École Centrale de Nantes (ECN)-Centre National de la Recherche Scientifique (CNRS)-IMT Atlantique (IMT Atlantique)
Jazyk: angličtina
Rok vydání: 2018
Předmět:
Predicate logic
Discrete mathematics
Normalization (statistics)
ACM: F.: Theory of Computation/F.4: MATHEMATICAL LOGIC AND FORMAL LANGUAGES/F.4.1: Mathematical Logic/F.4.1.7: Proof theory
010102 general mathematics
[INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO]
020207 software engineering
02 engineering and technology
ACM: F.: Theory of Computation/F.3: LOGICS AND MEANINGS OF PROGRAMS/F.3.2: Semantics of Programming Languages/F.3.2.2: Operational semantics
Axiom of dependent choice
Lambda
01 natural sciences
TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES
TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS
Computer Science::Logic in Computer Science
Realizability
0202 electrical engineering
electronic engineering
information engineering

ACM: F.: Theory of Computation/F.3: LOGICS AND MEANINGS OF PROGRAMS/F.3.3: Studies of Program Constructs/F.3.3.0: Control primitives
0101 mathematics
Lambda calculus
computer
Mathematics
computer.programming_language
ACM: F.: Theory of Computation/F.3: LOGICS AND MEANINGS OF PROGRAMS/F.3.3: Studies of Program Constructs/F.3.3.4: Type structure
Zdroj: FOSSACS 18-21st International Conference on Foundations of Software Science and Computation Structures
FOSSACS 18-21st International Conference on Foundations of Software Science and Computation Structures, Apr 2018, Thessalonique, Greece. pp.276-292, ⟨10.1007/978-3-319-89366-2_15⟩
Lecture Notes in Computer Science ISBN: 9783319893655
FoSSaCS
Popis: International audience; We define a variant of realizability where realizers are pairs of a term and a substitution. This variant allows us to prove the normalization of a simply-typed call-by-need λ-calculus with control due to Ariola et al. Indeed, in such call-by-need calculus, substitutions have to be delayed until knowing if an argument is really needed. In a second step, we extend the proof to a call-by-need λ-calculus equipped with a type system equivalent to classical second-order predicate logic, representing one step towards proving the normalization of the call-by-need classical second-order arithmetic introduced by the second author to provide a proof-as-program interpretation of the axiom of dependent choice.
Databáze: OpenAIRE