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 |
Externí odkaz: |