Abstract
We investigate a category theoretic model where both “variables” and “names”, usually viewed as separate notions, are particular cases of the more general notion of distinction. The key aspect of this model is to consider functors over the category of irreflexive, symmetric finite relations. The models previously proposed for the notions of “variables” and “names” embed faithfully in the new one, and initial algebra/final coalgebra constructions can be transferred from the formers to the latter. Moreover, the new model admits a definition of distinction-aware simultaneous substitutions. As a substantial application example, we give the first semantic interpretation of Miller-Tiu’s \(FO\lambda^{\nabla}\) logic.
Work supported by EU projects IST-2001-33100 profundis and IST-510996 types.
Chapter PDF
Similar content being viewed by others
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
Adamek, J. (ed.): Coalgebraic Methods in Computer Science. ENTCS (2004)
Boreale, M., Buscemi, M.G., Montanari, U.: D-fusion: A distinctive fusion calculus. In: Chin, W.-N. (ed.) APLAS 2004. LNCS, vol. 3302, pp. 296–310. Springer, Heidelberg (2004)
Day, B.J.: On closed categories of functors. In: Reports of the Midwest Category Seminar. Lecture Notes in Mathematics, vol. 137, pp. 1–38. Springer, Heidelberg (1970)
Fiore, M., Staton, S.: Comparing operational models of name-passing process calculi. In: Adamek [1]
Fiore, M., Turi, D.: Semantics of name and value passing. In: Mairson, H. (ed.) Proc. 16th LICS, pp. 93–104. IEEE, Los Alamitos (2001)
Fiore, M., Plotkin, G., Turi, D.: Abstract syntax and variable binding. In: [11]
Gabbay, M., Cheney, J.: A sequent calculus for nominal logic. In: Proc. LICS 2004, pp. 139–148. IEEE Computer Society, Los Alamitos (2004)
Gabbay, M.J., Pitts, A.M.: A new approach to abstract syntax with variable binding. Formal Aspects of Computing 13, 341–363 (2002)
Ghani, N., Yemane, K., Victor, B.: Relationally staged computation in calculi of mobile processes. In: Adamek [1]
Hofmann, M.: Semantical analysis of higher-order abstract syntax. In: Longo [11]
Longo, G. (ed.): Proc. 14th Symp. of Logic in Computer Science. IEEE, Los Alamitos (1999)
Mac Lane, S., Moerdijk, I.: Sheaves in Geometry and Logic. Springer, Heidelberg (1994)
Miculan, M., Scagnetto, I.: A framework for typed HOAS and semantics. In: Proc. PPDP 2003, pp. 184–194. ACM Press, New York (2003)
Miculan, M., Yemane, K.: A unifying model of variables and names. TR UDMI/15/2004/RR, Dept. of Mathematics and Computing Science, Univ. of Udine (2004), http://www.dimi.uniud.it/miculan/Papers/UDMI152004.pdf
Miller, D., Tiu, A.F.: A proof theory for generic judgments: An extended abstract. In: LICS 2003, pp. 118–127. IEEE, Los Alamitos (2003)
Pitts, A.M.: Categorical logic. In: Handbook of LICS, vol. 5. OUP (2000)
Pitts, A.M.: Nominal logic, a first order theory of names and binding. Information and Computation 186, 165–193 (2003)
Power, J., Tanaka, M.: Binding signatures for generic contexts. In: Urzyczyn, P. (ed.) TLCA 2005. LNCS, vol. 3461, pp. 308–323. Springer, Heidelberg (2005)
Stark, I.: A fully abstract domain model for the π-calculus. In: Proc. LICS 1996 (1996)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Miculan, M., Yemane, K. (2005). A Unifying Model of Variables and Names. In: Sassone, V. (eds) Foundations of Software Science and Computational Structures. FoSSaCS 2005. Lecture Notes in Computer Science, vol 3441. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-31982-5_11
Download citation
DOI: https://doi.org/10.1007/978-3-540-31982-5_11
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-25388-4
Online ISBN: 978-3-540-31982-5
eBook Packages: Computer ScienceComputer Science (R0)