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 条
  • [21] A Core Calculus for Equational Proofs of Cryptographic Protocols
    Gancher, Joshua
    Sojakova, Kristina
    Fan, Xiong
    Shi, Elaine
    Morrisett, Greg
    PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL, 2023, 7 (POPL): : 866 - 892
  • [22] Cyclic proofs for the first-order μ-calculus
    AFSHARI, B. A. H. A. R. E. H.
    ENQVIST, S. E. B. A. S. T. I. A. N.
    LEIGH, G. R. A. H. A. M. E.
    LOGIC JOURNAL OF THE IGPL, 2024, 32 (01) : 1 - 34
  • [23] A calculus of circular proofs and its categorical semantics
    Santocanale, L
    FOUNDATIONS OF SOFTWARE SCIENCE AND COMPUTATION STRUCTURES, PROCEEDINGS, 2002, 2303 : 357 - 371
  • [24] Normalization proofs for the un-typed μμ′-calculus
    Battyanyi, Peter
    Nour, Karim
    AIMS MATHEMATICS, 2020, 5 (04): : 3702 - 3713
  • [25] FUNCTION THEORY IN AN AXIOM-FREE EQUATION CALCULUS
    Goodstein, R. L.
    PROCEEDINGS OF THE LONDON MATHEMATICAL SOCIETY, 1945, 48 : 401 - 434
  • [26] Abstract interpretation of proofs: Classical propositional calculus
    Hyland, M
    COMPUTER SCIENCE LOGIC, PROCEEDINGS, 2004, 3210 : 6 - 21
  • [27] Loop-free calculus for modal logic . II
    Andrikonis, Julius
    LITHUANIAN MATHEMATICAL JOURNAL, 2012, 52 (02) : 123 - 133
  • [28] Alternative proofs for the type II free Poisson variables and for the free compression results - Appendix
    Voiculescu, D
    AMERICAN JOURNAL OF MATHEMATICS, 1996, 118 (04) : 832 - 837
  • [29] Lambda calculus, type theory, and natural language II
    Fox, Chris
    Fernandez, Maribel
    Lappin, Shalom
    JOURNAL OF LOGIC AND COMPUTATION, 2008, 18 (02) : 204 - 204
  • [30] PRESERVATION OF STRONG NORMALISATION MODULO PERMUTATIONS FOR THE STRUCTURAL λ-CALCULUS
    Accattoli, Beniamino
    Kesner, Delia
    LOGICAL METHODS IN COMPUTER SCIENCE, 2012, 8 (01)
12345