Abstract
We present a realizability interpretation of co-inductive types based on partial equivalence relations (per's). We extract from the per's interpretation sound rules to type recursive definitions. These recursive definitions are needed to introduce ‘infinite’ and ‘total’ objects of co-inductive type such as an infinite stream, a digital transducer, or a non-terminating process. We show that the proposed type system subsumes those studied by Coquand and Gimenez while still enjoying the basic syntactic properties of subject reduction and strong normalization with respect to a confluent rewriting system first put forward by Gimenez.
The first author was partially supported by CTI-CNET 95-1B-182, Action Incitative INRIA, IFCPAR 1502-1, WG Confer, and HCM Express. A preliminary version of this paper (including proofs) can be found in [1].
Chapter PDF
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
R. Amadio and S. Coupet-Grimal. Analysis of a guard condition in type theory (preliminary report). Technical Report TR 1997.245. Also appeared as RR-INRIA 3300, Université de Provence (LIM), 1997. Available at http://protis.univ-mrs.fr/~amadio.
H. Barendregt. The lambda calculus; its syntax and semantics. North-Holland, 1984.
Coq-project. The Coq proof assistant reference manual. Available at http://pauillac.inria.fr/coq, 1996.
T. Coquand. Infinite objects in type theory. In Types for proofs and programs, Springer Lect. Notes in Comp. Sci. 806, 1993.
T. Coquand and G. Huet. A calculus of constructions. Information and Computation, 76:95–120, 1988.
S. Coupet-Grimal and L. Jakubiec. Coq and hardware verification: a case study. In Proc. TPHOL, Springer Lect. Notes in Comp. Sci. 1125, 1996.
H. Geuvers. Inductive and coinductive types with iteration and recursion. In Proc. of Workshop on types for proofs and programs, Nordström et al. (eds.), pages 193–217, 1992. Available electronically.
E. Gimenez. Un calcul de constructions infinies et son application à la vérification de systèmes communicants. PhD thesis, ENS Lyon, 1996.
E. Gimenez. Personal communication. October 1997.
J.-Y. Girard, Y.Lafont, and P. Taylor. Proofs and Types. Cambridge University Press, 1989.
F. Leclerc and C. Paulin-Morhing. Programming with streams in Coq. A case study: the sieve of Eratosthenes. In Proc. TYPES, Springer Lect. Notes in Comp. Sci. 806, 1993.
R. Loader. Equational theories for inductive types. Annals of Pure and Applied Logic, 84:175–218, 1997.
G. Longo and E. Moggi. Constructive natural deduction and its modest interpretation. Mathematical Structures in Computer Science, 1:215–254, 1992.
N. Mendler. Recursive types and type constraints in second-order lambda calculus. In Proc. IEEE Logic in Comp. Sci., 1987.
M. Nesi. A formalization of the process algebra CCS in higher order logic. Technical Report 278, Computer Laboratory, University of Cambridge, December 1992.
L. Paulson. Mechanizing coinduction and corecursion in higher-order logic. J. of Logic and Computation, 7(2):175–204, 1997.
C. Raffalli. L'arithmétique fonctionnelle du second ordre avec point fixes. PhD thesis, Université Paris VII, 1994.
A. Salomaa. Two complete systems for the algebra of complete events. Journal of the ACM, 13–1, 1966.
D. Scott. Data types as lattices. SIAM J. of Computing, 5:522–587, 1976.
M. Tatsuta. Realizability interpretation of coinductive definitions and program synthesis with streams. Theoretical Computer Science, 122:119–136, 1994.
S. Thompson. Haskell. The craft of functional programming. Addison-Wesley, 1996.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1998 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Amadio, R.M., Coupet-Grimal, S. (1998). Analysis of a guard condition in type theory. In: Nivat, M. (eds) Foundations of Software Science and Computation Structures. FoSSaCS 1998. Lecture Notes in Computer Science, vol 1378. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0053541
Download citation
DOI: https://doi.org/10.1007/BFb0053541
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-64300-5
Online ISBN: 978-3-540-69720-6
eBook Packages: Springer Book Archive