slepice: towards a verified implementation of type theory in type theory. (English) Zbl 07496645
Fernández, Maribel (ed.), Logic-based program synthesis and transformation. 30th international symposium, LOPSTR 2020, Bologna, Italy, September 7–9, 2020. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12561, 133-150 (2021).
Summary: Dependent types have proven a useful technique for development of verified software. Despite the existence of many systems based in dependent type theory, mostly interactive theorem provers but also programming languages, there is no system that would itself be implemented using dependent types. Recently, a new approach to type inference and term synthesis for type theory with dependent types emerged that separates the process into an analysis phase that is carried out in type theory, and a search phase that is carried out in a logic programming engine.
We describe an architecture of type inference and term synthesis engine for a language with dependent types that is based on the new approach and that is feasible to implement using a dependently typed language. We demonstrate the architecture by describing slepice, its particular implementation.
For the entire collection see [Zbl 1482.68019].
We describe an architecture of type inference and term synthesis engine for a language with dependent types that is based on the new approach and that is feasible to implement using a dependently typed language. We demonstrate the architecture by describing slepice, its particular implementation.
For the entire collection see [Zbl 1482.68019].
MSC:
| 68N30 | Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) |
Keywords:
dependent types; type inference; Horn clause logic; term synthesis; proof-relevant resolutionReferences:
| [1] | Abel, A.; Öhman, J.; Vezzosi, A., Decidability of conversion for type theory in type theory, PACMPL, 2, POPL, 23:1-23:29 (2018) · doi:10.1145/3158111 |
| [2] | Anand, A.; Boulier, S.; Cohen, C.; Sozeau, M.; Tabareau, N.; Avigad, J.; Mahboubi, A., Towards certified meta-programming with typed template-coq, Interactive Theorem Proving, 20-39 (2018), Cham: Springer, Cham · Zbl 1468.68071 · doi:10.1007/978-3-319-94821-8_2 |
| [3] | Appel, AW; Michael, NG; Stump, A.; Virga, R., A trustworthy proof checker, J. Autom. Reas., 31, 3-4, 231-260 (2003) · Zbl 1069.68596 · doi:10.1023/B:JARS.0000021013.61329.58 |
| [4] | Bertot, Y., Castéran, P.: Interactive theorem proving and program development - coq’art: the calculus of inductive constructions. In: Texts in Theoretical Computer Science. An EATCS Series. Springer, Heidelberg (2004). doi:10.1007/978-3-662-07964-5 · Zbl 1069.68095 |
| [5] | Brady, E., Idris, a general-purpose dependently typed programming language: design and implementation, J. Funct. Program., 23, 5, 552-593 (2013) · Zbl 1295.68059 · doi:10.1017/S095679681300018X |
| [6] | Cockx, J.: type theory unchained: extending agda with user-defined rewrite rules. In: Bezem, M., Mahboubi, A. (eds.) 25th International Conference on Types for Proofs and Programs, TYPES 2019, Oslo, Norway, 11-14 June 2019, LIPIcs 175, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, pp. 2:1-2:27 (2019). doi:10.4230/LIPIcs.TYPES.2019.2 |
| [7] | Dowek, G.; Bezem, M.; Groote, JF, The undecidability of typability in the Lambda-Pi-calculus, Typed Lambda Calculi and Applications, 139-145 (1993), Heidelberg: Springer, Heidelberg · Zbl 0788.68017 · doi:10.1007/BFb0037103 |
| [8] | Dunchev, C.; Guidi, F.; Sacerdoti Coen, C.; Tassi, E.; Davis, M.; Fehnker, A.; McIver, A.; Voronkov, A., ELPI: fast, embeddable, \( \lambda\) prolog interpreter, Logic for Programming, Artificial Intelligence, and Reasoning, 460-468 (2015), Heidelberg: Springer, Heidelberg · Zbl 1471.68046 · doi:10.1007/978-3-662-48899-7_32 |
| [9] | Farka, F.; Komendantskaya, E.; Hammond, K., Proof-relevant horn clauses for dependent type inference and term synthesis, Theory Pract. Log. Program., 18, 3-4, 484-501 (2018) · Zbl 1451.68323 · doi:10.1017/S1471068418000212 |
| [10] | Fu, P.; Komendantskaya, E., Operational semantics of resolution and productivity in Horn clause logic, Formal Aspects Comput., 29, 3, 453-474 (2016) · Zbl 1362.68048 · doi:10.1007/s00165-016-0403-1 |
| [11] | Geuvers, H.; Barendsen, E., Some logical and syntactical observations concerning the first-order dependent type system lambda-P, Math. Struct. Comput. Sci., 9, 4, 335-359 (1999) · Zbl 0939.03016 · doi:10.1017/S0960129599002856 |
| [12] | Guidi, F.; Coen, CS; Tassi, E., Implementing type theory in higher order constraint logic programming, Math. Struct. Comput. Sci., 29, 8, 1125-1150 (2019) · Zbl 1430.68025 · doi:10.1017/S0960129518000427 |
| [13] | Harper, R.; Pfenning, F., On equivalence and canonical forms in the LF type theory, ACM T. Comp. Log., 6, 1, 61-101 (2005) · Zbl 1367.03055 · doi:10.1145/1042038.1042041 |
| [14] | Leroy, X., Blazy, S., Kästner, D., Schommer, B., Pister, M., Ferdinand, C.: CompCert - a formally verified optimizing compiler. In: ERTS 2016: Embedded Real Time Software and Systems, 8th European Congress, SEE, Toulouse, France (2016). https://hal.inria.fr/hal-01238879 |
| [15] | Norell, U.: Towards a practical programming language based on dependent type theory. Ph.D. thesis (2007) |
| [16] | Pientka, B., An insider’s look at LF type reconstruction: everything you (n)ever wanted to know, J. Funct. Program., 23, 1, 1-37 (2013) · Zbl 1262.68030 · doi:10.1017/S0956796812000408 |
| [17] | Pientka, B., Dunfield, J.: Beluga: a framework for programming and reasoning with deductive systems (system description). In: Proceedings of IJCAR 2010, pp. 15-21 (2010). doi:10.1007/978-3-642-14203-1_2 · Zbl 1291.68366 |
| [18] | Sewell, P., et al.: Ott: effective tool support for the working semanticist. In: Hinze, R., Ramsey, N. (eds.) Proceedings of the 12th ACM SIGPLAN International Conference on Functional Programming, ICFP 2007, Freiburg, Germany, 1-3 October 2007, pp. 1-12. ACM (2007). doi:10.1145/1291151.1291155 · Zbl 1291.68238 |
| [19] | Sozeau, M., The MetaCoq project, J. Autom. Reason., 64, 5, 947-999 (2020) · Zbl 1468.68075 · doi:10.1007/s10817-019-09540-0 |
| [20] | Sozeau, M.; Boulier, S.; Forster, Y.; Tabareau, N.; Winterhalter, T., Coq Coq correct! verification of type checking and erasure for Coq in Coq, PACMPL, 4, POPL, 8:1-8:28 (2020) · doi:10.1145/3371076 |
| [21] | Urban, C.; Cheney, J.; Berghofer, S., Mechanizing the metatheory of LF, ACM Trans. Comput. Log., 12, 2, 15:1-15:42 (2011) · Zbl 1351.68250 · doi:10.1145/1877714.1877721 |
| [22] | Urban, CU; Pitts, AM; Gabbay, M., Nominal unification, Theor. Comput. Sci., 323, 1-3, 473-497 (2004) · Zbl 1078.68140 · doi:10.1016/j.tcs.2004.06.016 |
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.
