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 条
  • [41] A FORGOTTEN THEORY OF PROOFS?
    Engeler, E.
    LOGICAL METHODS IN COMPUTER SCIENCE, 2019, 15 (03)
  • [42] A DPLL-based calculus for ground satisfiability modulo theories
    Tinelli, C
    LOGICS IN ARTIFICIAL INTELLIGENCE 8TH, 2002, 2424 : 308 - 319
  • [43] A Congruence Modulo Four for Real Schubert Calculus with Isotropic Flags
    Hein, Nickolas
    Sottile, Frank
    Zelenko, Igor
    CANADIAN MATHEMATICAL BULLETIN-BULLETIN CANADIEN DE MATHEMATIQUES, 2017, 60 (02): : 309 - 318
  • [44] The stratified foundations as a theory modulo
    Dowek, G
    TYPED LAMBDA CALCULI AND APPLICATIONS, PROCEEDINGS, 2001, 2044 : 136 - 150
  • [45] A Survey of Satisfiability Modulo Theory
    Monniaux, David
    COMPUTER ALGEBRA IN SCIENTIFIC COMPUTING, CASC 2016, 2016, 9890 : 401 - 425
  • [46] Superposition modulo a Shostak theory
    Ganzinger, H
    Hillenbrand, T
    Waldmann, U
    AUTOMATED DEDUCTION - CADE-19, PROCEEDINGS, 2003, 2741 : 182 - 196
  • [47] Linear lower bound on degrees of Positivstellensatz calculus proofs for the parity
    Grigoriev, D
    THEORETICAL COMPUTER SCIENCE, 2001, 259 (1-2) : 613 - 622
  • [48] SOME APPLICATIONS OF FREE DIFFERENTIAL-CALCULUS IN GROUP-THEORY
    SHPILRAIN, VE
    MATHEMATICAL NOTES, 1991, 49 (3-4) : 334 - 335
  • [49] An introduction to fuzzy propositional calculus using proofs from assumptions
    Tabakow, Iwan
    KNOWLEDGE-BASED INTELLIGENT INFORMATION AND ENGINEERING SYSTEMS, PT 2, PROCEEDINGS, 2006, 4252 : 187 - 194
  • [50] A calculus for modular loop acceleration and non-termination proofs
    Frohn, Florian
    Fuhs, Carsten
    INTERNATIONAL JOURNAL ON SOFTWARE TOOLS FOR TECHNOLOGY TRANSFER, 2022, 24 (05) : 691 - 715
12345