×

Pure type systems with explicit substitutions. (English) Zbl 1420.68038

Summary: We introduce a new formulation of pure type systems (PTSs) with explicit substitution and de Bruijn indices and formally prove some of its meta-theory. Using techniques based on Normalisation by Evaluation, we prove that untyped conversion can be typed for predicative PTSs. Although this equivalence was settled by Siles and Herbelin for the conventional presentation of PTSs, we strongly conjecture that our proof method can also be applied to PTSs with \(\eta\).

MSC:

68N18 Functional programming and lambda calculus
03B40 Combinatory logic and lambda calculus

Software:

Matita; Coq; Automath
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] AbadiM., CardelliL., CurienP.-L., & LévyJ. J. (1990) Explicit substitutions. In Proceedings of the 17th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages POPL ’90: San Francisco, California, USA, January 1990. ACM, pp. 31-46.
[2] AbelA. (2010) Towards normalization by evaluation for the βη-calculus of constructions. In Functional and Logic Programming, BlumeM., KobayashiN. & VidalG. (eds), Lectures Notes in Computer Science, vol. 6009. Sendai, Japan, April 19-21, 2010, Berlin Heidelberg: Springer, pp. 224-239. · Zbl 1284.68120
[3] AbelA., CoquandT. & DybjerP. (2007) Normalization by evaluation for Martin-Löf type theory with typed equality judgements. In Lics. Wrocław, Poland, July 10-14 2007. IEEE Computer Society, pp. 3-12.
[4] AbelA., CoquandT. & DybjerP. (2008) Verifying a semantic βη-conversion test for Martin-Löf type theory. In Proceedings of the 9th International Conference on Mathematics of Program Construction, MPC 2008, Marseille (Luminy), France, 15-18 July 2008, AudebaudP. & Paulin-MohringC. (eds), Lectures Notes in Computer Science, vol. 5133. Springer, pp. 29-56. · Zbl 1157.68025
[5] AbelA., CoquandT. & PaganoM. (2011) A modular type-checking algorithm for type theory with singleton types and proof irrelevance. Log. Methods Comput. Sci.7(2:4), 1-57.2794382 · Zbl 1213.68199
[6] AbramskyS. & JungA. (1994) Domain Theory. Oxford University Press. pp. 1-168.
[7] AdamsR. (2006) Pure type systems with judgemental equality. J. Funct. Program.16(2), 219-246.2203052 · Zbl 1088.68030
[8] AltenkirchT. & ChapmanJ. (2009) Big-step normalisation. J. Funct. Program.19(3-4), 311-333.10.1017/S09567968090072782541351 · Zbl 1191.68153 · doi:10.1017/S0956796809007278
[9] AspertiA., RicciottiW., CoenC. S. & TassiE. (2011) The Matita interactive theorem prover. In Cade, Wrocław, Poland, 31 July-5 August 2011, BjørnerN. & Sofronie-StokkermansV. (eds), Lecture Notes in Computer Science, vol. 6803. Springer, pp. 64-69. · Zbl 1341.68179
[10] BarendregtH. (1992) Lambda calculi with types. In Handbook of Logic in Computer Science, AbramskyS., GabbayD. M., & MaibaumT. S. E. (eds), Oxford University Press, pp. 117-309.
[11] BarrasB. (1998) Verification of the interface of a small proof system in coq. In Types for Proofs and Programs, Aussois, France, December 15-19, 1996, GiménezE. & Paulin-MohringC. (eds), Lectures Notes in Computer Science, vol. 1512. Berlin Heidelberg: Springer, pp. 28-45. · Zbl 0927.03018
[12] BartheG. & CoquandT. (2006) Remarks on the equational theory of non-normalizing pure type systems.J. Funct. Program.16, 137-155.2203049 · Zbl 1088.68033
[13] BartheG. & SørensenM. H. (2000) Domain-free pure type systems. J. Funct. Program.10(5), 417-452.10.1017/S09567968000037501797516 · Zbl 0979.03013 · doi:10.1017/S0956796800003750
[14] BlooR. (2001) Pure type systems with explicit substitution. Math. Struct. Comput. Sci.11(1), 3-19.10.1017/S096012950000325X1828137 · Zbl 0972.68026 · doi:10.1017/S096012950000325X
[15] Coq, Development Team. (2004) The Coq Proof Assistant Reference Manual. Version 8.0.
[16] CurienP.-L., HardinT. & LévyJ.-J. (1996) Confluence properties of weak and strong calculi of explicit substitutions.J. Assoc. Comput. Mach.43, 362-397.10.1145/226643.226675 · Zbl 0885.03014 · doi:10.1145/226643.226675
[17] CurienP.-L., HardinT. & RíosA. (1992) Strong normalization of substitutions. In Mfcs, Prague, Czechoslovakia, August 24-28, 1992, HavelI. M., & KoubekV. (eds), Lectures Notes in Computer Science, vol. 629. Springer, pp. 209-217. · Zbl 1496.03059
[18] DanielssonN. A. (2007) A formalisation of a dependently typed language as an inductive-recursive family. In Types for Proofs and Programs, Cividale del Friuli, Italy, May 2-5, 2007, AltenkirchT. & McBrideC. (eds), Lecture Notes in Computer Science, vol. 4502. Berlin Heidelberg: Springer, pp. 93-109. · Zbl 1178.03026
[19] DybjerP. (1996) Internal type theory. In Types for Proofs and Programs, International Workshop, TYPES’95, Torino, Italy, June 5-8, 1995, BerardiS. & CoppoM. (eds), Lectures Notes in Computer Science, vol. 1158. Springer, pp. 120-134. · Zbl 1434.03149
[20] DybjerP. (2000) A general formulation of simultaneous inductive-recursive definitions in type theory. J. Symb. Log.65(2), 525-549.10.2307/2586554 · Zbl 0960.03048 · doi:10.2307/2586554
[21] FridlenderD. & PaganoM. (2013) A type-checking algorithm for Martin-Löf type theory with subtyping based on normalisation by evaluation. In Typed Lambda Calculi and Applications, Eindhoven, The Netherlands, 26-28 June 2013, HasegawaM. (ed), Lecture Notes in Computer Science, vol. 7941. Berlin Heidelberg: Springer, pp. 140-155. · Zbl 1273.03106
[22] GeuversH. (1993) Logics and Type Systems. Ph.D. thesis, Katholieke Universiteit Nijmegen.
[23] GeuversH., & WernerB. (1994) On the Church-Rosser property for expressive type systems and its consequences for their metatheoretic study. In Proceedings Symposium on Logic in Computer Science, 1994. LICS ’94, Paris, France, July 4-7, 1994. pp. 320-329.
[24] HardinT. (1989) Confluence results for the pure strong categorical logic CCL: Lambda-Calculi as subsystems of CCL. Theor. Comput. Sci.65(3), 291-342.10.1016/0304-3975(89)90105-91006431 · Zbl 0707.03012 · doi:10.1016/0304-3975(89)90105-9
[25] KesnerD. (2000) Confluence of extensional and non-extensional λ-calculi with explicit substitutions. Theor. Comput. Sci.238(1-2), 183-220.10.1016/S0304-3975(98)00166-21760482 · Zbl 0944.68033 · doi:10.1016/S0304-3975(98)00166-2
[26] LuoZ. (1994) Computation and Reasoning: A Type Theory for Computer Science. International Series of Monographs on Computer Science. Clarendon Press.1291601 · Zbl 0823.68101
[27] MiquelA. & WernerB. (2002) The not so simple proof-irrelevant model of CC. In Types, Berg en Dal, The Netherlands, April 24-28, 2002, GeuversH. & WiedijkF. (eds), Lecture Notes in Computer Science, vol. 2646. Springer, pp. 240-258. · Zbl 1023.03024
[28] MuñozC. (2001) Dependent types and explicit substitutions: A meta-theoretical development.Math. Struct. Comput. Sci.11, 91-129.10.1017/S09601295000032611828140 · Zbl 0976.03014 · doi:10.1017/S0960129500003261
[29] SilesV. (2010) Investigation on the Typing of Equality in Type Systems. Ph.D. thesis, École Polytechnique.
[30] SilesV. & HerbelinH. (2010) Equality is typable in semi-full pure type systems. In Lics. Edinburgh, Scotland, UK, July 11-14, 2010, IEEE Computer Soc. Press, pp. 21-30.
[31] SilesV. & HerbelinH. (2012) Pure type System conversion is always typable. J. Funct. Program.22(2), 153-180.10.1017/S09567968120000442923649 · Zbl 1271.68080 · doi:10.1017/S0956796812000044
[32] StreicherT. (1989) Correctness and Completeness of a Categorical Semantics of the Calculus of Constructions. Ph.D. thesis, Universität Passau, Passau, West Germany.
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.