No CrossRef data available.
Article contents
A semantics for nabla
Published online by Cambridge University Press: 17 April 2018
Abstract
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.
- Type
- Paper
- Information
- Copyright
- © Cambridge University Press 2018
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
Schöpp, U. (2007). Modelling generic judgments. Electronic Notes in Theoretical Computer Science 174 (5) 19–35.CrossRefGoogle Scholar