Hostname: page-component-74656f9884-8r8nv Total loading time: 0 Render date: 2026-11-07T19:58:05.720Z Has data issue: false hasContentIssue false
  • English
  • Français

A semantics for nabla

Published online by Cambridge University Press:  17 April 2018

JEAN GOUBAULT-LARRECQ Open the ORCID record for JEAN GOUBAULT-LARRECQ [Opens in a new window]
JEAN GOUBAULT-LARRECQ*
Affiliation:
LSV, ENS Paris-Saclay, CNRS, Université Paris-Saclay, 94230 Cachan, France Email: goubault@lsv.fr
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the 'Save PDF' action button.

We give a semantics for a classical variant of Dale Miller and Alwen Tiu’s logic FOλ∇. Our semantics validates the rule that nabla x implies exists x, but is otherwise faithful to the authors’ original intentions. The semantics is based on a category of so-called nabla sets, which are simply strictly increasing sequences of non-empty sets. We show that the logic is sound for that semantics. Assuming there is a unique base type ι, we show that it is complete for Henkin structures, incomplete for standard structures in general, but complete for standard structures in the case of Π1 formulae, and that includes all first-order formulae.

Footnotes

†

A variant of this paper was presented at Dale Miller’s 60th birthday. The current presentation is simpler, although essentially equivalent. We have also taken the opportunity to correct a mistake in the proof of Proposition 8.4.

References

Bucalo, A., Honsell, F., Miculan, M., Scagnetto, I. and Hofmann, M. (2006). Consistency of the theory of contexts. Journal of Functional Programming 16 (3) 327–372.CrossRefGoogle Scholar
Cervesato, I., Durgin, N. A., Lincoln, P. D., Mitchell, J. C. and Scedrov, A. (1999). A meta-notation for protocol analysis. In: Proceedings of the 12th IEEE Computer Security Foundations Workshop, IEEE Conference Publications, 55–69.CrossRefGoogle Scholar
Curien, P.-L. (1993). Categorical Combinators, Sequential Algorithms, and Functional Programming. Birkhäuser, Boston, MA.CrossRefGoogle Scholar
Fitting, M. (1996). First-Order Logic and Automated Theorem Proving. Graduate Texts in Computer Science. Spring Verlag, 2nd edition.CrossRefGoogle Scholar
Friedman, H. (1975). Equality between functionals. In: Parikh, P. (ed.) Logic Colloquium 1972–73, Lecture Notes in Mathematics, vol. 453, Springer-Verlag, 22–37.Google Scholar
Gabbay, M. J. and Pitts, A. M. (1999). A new approach to abstract syntax involving binders. In: 14th Annual Symposium on Logic in Computer Science, IEEE Computer Society Press, Washington, 214–224.Google Scholar
Gacek, A. (2008). The Abella interactive theorem prover (system description). In: Armando, A., Baumgartner, A. and Dowek, G. (eds.) Proceedings of IJCAR, Lecture Notes in Artificial Intelligence, vol. 5195, Springer, 154–161.Google Scholar
Hofmann, M. (1999). Semantical analysis of higher-order abstract syntax. In: Proceedings of the 14th Annual IEEE Symposium on Logics in Computer Science (LICS’99), IEEE, 204–213.CrossRefGoogle Scholar
Miculan, M. and Yemane, K. (2005). A unifying model of variables and names. In: Proceedings of 8th Intl. Conf. Foundations of Software Science and Computational Structures (FOSSACS’05), held as part of the Joint European Conferences on Theory and Practice of Software (ETAPS’05), LNCS, Springer Verlag, Edinburgh, UK, 3441.Google Scholar
Miller, D. (1992). The pi-calculus as a theory in linear logic: Preliminary results. Technical Report MS-CIS-92-48, University of Pennsylvania (CIS), October.Google Scholar
Miller, D. and Tiu, A. (2005). A proof theory for generic judgments. Transactions on Computational Logic 6 (4) 749–783.CrossRefGoogle Scholar
Mitchell, J. C. (1985). Foundations for Programming Languages, MIT Press.Google Scholar
Schöpp, U. (2007). Modelling generic judgments. Electronic Notes in Theoretical Computer Science 174 (5) 19–35.CrossRefGoogle Scholar