Proofs for Free in the λII-Calculus Modulo Theory

被引：0
|
作者：
Traversie, Thomas [1 ,2 ]
机构：
[1] Univ Paris Saclay, CentraleSupelec, MICS, Gif Sur Yvette, France
[2] Univ Paris Saclay, Inria, CNRS, LMO,ENS Paris Saclay, Gif Sur Yvette, France
来源：
ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE | 2024年 / 404期
关键词：
D O I：
10.4204/EPTCS.404.4
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
Parametricity allows the transfer of proofs between different implementations of the same data structure. The lambda II-calculus modulo theory is an extension of the lambda-calculus with dependent types and user-defined rewrite rules. It is a logical framework, used to exchange proofs between different proof systems. We define an interpretation of theories of the lambda II-calculus modulo theory, inspired by parametricity. Such an interpretation allows to transfer proofs for free between theories that feature the notions of proposition and proof, when the source theory can be embedded into the target theory.
引用
收藏
页数：69
相关论文
共 50 条
  • [1] From Rewrite Rules to Axioms in the λΠ-Calculus Modulo Theory
    Blot, Valentin
    Dowek, Gilles
    Traversie, Thomas
    Winterhalter, Theo
    FOUNDATIONS OF SOFTWARE SCIENCE AND COMPUTATION STRUCTURES, PT II, FOSSACS 2024, 2024, 14575 : 3 - 23
  • [2] Reducibility Proofs in the λ-Calculus
    Kamareddine, Fairouz
    Rahli, Vincent
    Wells, J. B.
    FUNDAMENTA INFORMATICAE, 2012, 121 (1-4) : 121 - 152
  • [3] Kuroda's Translation for the XII-Calculus Modulo Theory and Dedukti
    Traversie, Thomas
    ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2024, (404):
  • [4] Checking Zenon Modulo Proofs in Dedukti
    Cauderlier, Raphael
    Halmagrand, Pierre
    ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2015, (186): : 57 - 73
  • [5] Rewriting Modulo beta in the lambda Pi-Calculus Modulo
    Saillard, Ronan
    ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2015, (185): : 87 - 101
  • [6] A new graphical calculus of proofs
    Alves, Sandra
    Fernandez, Maribel
    Mackie, Ian
    ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2011, (48): : 69 - 84
  • [7] Socratic proofs for quantifiers (Calculus)
    Wisniewski, Andrzej
    Shangin, Vasilyi
    JOURNAL OF PHILOSOPHICAL LOGIC, 2006, 35 (02) : 147 - 178
  • [8] A resolution calculus for shortening proofs
    Peltier, Nicolas
    LOGIC JOURNAL OF THE IGPL, 2005, 13 (03) : 307 - 333
  • [9] Extensional proofs in a propositional logic modulo isomorphisms
    Diaz-Caro, Alejandro
    Dowek, Gilles
    THEORETICAL COMPUTER SCIENCE, 2023, 977
  • [10] Focus-Style Proofs for the Two-Way Alternation-Free μ-Calculus
    Rooduijn, Jan
    Venema, Yde
    LOGIC, LANGUAGE, INFORMATION, AND COMPUTATION, WOLLIC 2023, 2023, 13923 : 318 - 335
12345