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 条
12345