Abstract
The paper discusses semantics of encodings in logical frameworks where equalities in object calculi are represented by families of types as the case inELF. The notion of Leibniz equality in a category is introduced. Two morphisms in a category are Leibniz equal if they are seen so by an internal category. The usual categorical properties are then relativized tor-properties by requiring mediating morphisms to be unique up to some Leibniz equality. Using these terminologies, it is shown, by an example, that the term model of the encoding of an adequately represented object calculus is r-isomorphic to the term model of the object language.
This is a preview of subscription content, log in via an institution to check access.
Similar content being viewed by others
References
Nordström B, Petersson K, Smith J. Programming in Martin-Löf's Type Theory—An Introduction. Oxford University Press, Vol. 7 of International Series of Monographs on Computer Science, 1990.
Harper R, Honsell F, Plotkin G. A framework for defining logics.Journal of ACM, 1993, 40 (1): 143–184.
Fu Y X. Categorical properties of logical frameworks.Mathematical Structures in Computer Science, 1997, 7: 1–47.
Barr M, Wells C. Toposes, Triples and Theories. Spring-Verlag, 1985, Volume 278 of the Series of Comprehensive Studies in Mathematics.
Author information
Authors and Affiliations
Additional information
Supported by the National Natural Science Fund of China, grant number 69503006
FU Yuxi is an Associate Professor in the Department of Computer Science at Shanghai Jiao Tong University. He received his Ph. D. degree in computer science in 1992 from Manchester University, England. His current research interests include type theory, semantics and concurrency theory.
Rights and permissions
About this article
Cite this article
Fu, Y. Relative properties of frame language. J. Comput. Sci. & Technol. 14, 320–327 (1999). https://doi.org/10.1007/BF02948734
Received:
Revised:
Issue Date:
DOI: https://doi.org/10.1007/BF02948734