Guarded dependent type theory with coinductive types. (English) Zbl 1475.68060
Jacobs, Bart (ed.) et al., Foundations of software science and computation structures. 19th international conference, FOSSACS 2016, held as part of the European joint conferences on theory and practice of software, ETAPS 2016, Eindhoven, The Netherlands, April 2–8, 2016. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 9634, 20-35 (2016).
Summary: We present guarded dependent type theory, \(\mathsf {gDTT}\), an extensional dependent type theory with a “later” modality and clock quantifiers for programming and proving with guarded recursive and coinductive types. The later modality is used to ensure the productivity of recursive definitions in a modular, type based, way. Clock quantifiers are used for controlled elimination of the later modality and for encoding coinductive types using guarded recursive types. Key to the development of \(\mathsf {gDTT}\) are novel type and term formers involving what we call “delayed substitutions”. These generalise the applicative functor rules for the later modality considered in earlier work, and are crucial for programming and proving with dependent types. We show soundness of the type theory with respect to a denotational model.
For the entire collection see [Zbl 1333.68011].
For the entire collection see [Zbl 1333.68011].
MSC:
| 68N18 | Functional programming and lambda calculus |
| 03B38 | Type theory |
| 03B70 | Logic in computer science |
| 68N30 | Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) |
References:
| [1] | Abel, A., Pientka, B.: Wellfounded recursion with copatterns: A unified approach to termination and productivity. In: ICFP, pp. 185–196 (2013) · Zbl 1323.68087 · doi:10.1145/2500365.2500591 |
| [2] | Appel, A.W., Melliès, P.A., Richards, C.D., Vouillon, J.: A very modal model of a modern, major, general type system. In: POPL, pp. 109–122 (2007) · Zbl 1295.68072 · doi:10.1145/1190216.1190235 |
| [3] | Atkey, R., McBride, C.: Productive coprogramming with guarded recursion. In: ICFP, pp. 197–208 (2013) · Zbl 1323.68092 · doi:10.1145/2500365.2500597 |
| [4] | Birkedal, L., Møgelberg, R.E.: Intensional type theory with guarded recursive types qua fixed points on universes. In: LICS, pp. 213–222 (2013) · Zbl 1367.68060 · doi:10.1109/LICS.2013.27 |
| [5] | Birkedal, L., Møgelberg, R.E., Schwinghammer, J., Støvring, K.: First steps in synthetic guarded domain theory: step-indexing in the topos of trees. LMCS 8(4) (2012) · Zbl 1269.03035 |
| [6] | Bizjak, A., Grathwohl, H.B., Clouston, R., Møgelberg, R.E., Birkedal, L.: Guarded dependent type theory with coinductive types (2016). http://arxiv.org/abs/1601.01586 · Zbl 1475.68060 |
| [7] | Bizjak, A., Møgelberg, R.E.: A model of guarded recursion with clock synchronisation. In: MFPS (2015) · Zbl 1351.68057 |
| [8] | 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 |
| [9] | Clouston, R., Bizjak, A., Grathwohl, H.B., Birkedal, L.: Programming and reasoning with guarded recursion for coinductive types. In: FoSSaCS (2015) · Zbl 1459.68034 · doi:10.1007/978-3-662-46678-0_26 |
| [10] | Cohen, C., Coquand, T., Huber, S., Mörtberg, A.: Cubical type theory: a constructive interpretation of the univalence axiom, unpublished (2015) · Zbl 1434.03036 |
| [11] | Constable, R.L., Allen, S.F., Bromley, H.M., Cleaveland, W.R., Cremer, J.F., Harper, R.W., Howe, D.J., Knoblock, T.B., Mendler, N.P., Panangaden, P., Sasaki, J.T., Smith, S.F.: Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall Inc, Upper Saddle River, NJ, USA (1986) |
| [12] | Coquand, T.: Infinite objects in type theory. In: TYPES, pp. 62–78 (1993) |
| [13] | Giménez, E.: Codifying guarded definitions with recursive schemes. In: TYPES, pp. 39–59 (1995) · doi:10.1007/3-540-60579-7_3 |
| [14] | Hughes, J., Pareto, L., Sabry, A.: Proving the correctness of reactive systems using sized types. In: POPL, pp. 410–423 (1996) · doi:10.1145/237721.240882 |
| [15] | Jacobs, B.: Categorical Logic and Type Theory. Studies in Logic and the Foundations of Mathematics, vol. 141. North Holland, Amsterdam (1999) · Zbl 0911.03001 |
| [16] | Krishnaswami, N.R., Benton, N.: Ultrametric semantics of reactive programs. In: LICS, pp. 257–266 (2011) · doi:10.1109/LICS.2011.38 |
| [17] | The Coq development team: the coq proof assistant reference manual. LogiCal Project (2004). version 8.0. http://coq.inria.fr |
| [18] | McBride, C., Paterson, R.: Applicative programming with effects. J. Funct. Program. 18(1), 1–13 (2008) · Zbl 1128.68020 · doi:10.1017/S0956796807006326 |
| [19] | Møgelberg, R.E.: A type theory for productive coprogramming via guarded recursion. In: CSL-LICS (2014) · Zbl 1394.68066 · doi:10.1145/2603088.2603132 |
| [20] | Nakano, H.: A modality for recursion. In: LICS, pp. 255–266 (2000) · doi:10.1109/LICS.2000.855774 |
| [21] | Norell, U.: Towards a practical programming language based on dependent type theory. Ph.D. thesis, Chalmers University of Technology (2007) |
| [22] | Paviotti, M., Møgelberg, R.E., Birkedal, L.: A model of PCF in guarded type theory. In: MFPS (2015) · Zbl 1351.68063 |
| [23] | Svendsen, K., Birkedal, L.: Impredicative concurrent abstract predicates. In: Shao, Z. (ed.) ESOP 2014 (ETAPS). LNCS, vol. 8410, pp. 149–168. Springer, Heidelberg (2014) · Zbl 1405.68092 · doi:10.1007/978-3-642-54833-8_9 |
| [24] | The Univalent Foundations Program: Homotopy Type Theory: Univalent Foundations of Mathematics, Institute for Advanced Study (2013). http://homotopytypetheory.org/book |
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.
