A cartesian closed category in Martin-Löf’s intuitionistic type theory. (English) Zbl 1018.68078
Summary: First, we briefly recall the main definitions of the theory of information bases and translations. These mathematical structures are the basis to construct the cartesian closed category InfBas, which is equivalent to the category ScDom of Scott domains. Then, we show that all the definitions and the proof of all the properties that one needs in order to show that InfBas is indeed a cartesian closed category can be formalized within Martin-Löf’s intuitionistic type theory.
MSC:
| 68T27 | Logic in artificial intelligence |
| 03B15 | Higher-order logic; type theory (MSC2010) |
| 03B20 | Subsystems of classical logic (including intuitionistic logic) |
Keywords:
Scott domainsReferences:
| [1] | R. Backhouse, P. Chisholm, G. Malcom, E. Saaman, Do-it-yourself Type Theory, Formal Aspects of Computing, vol. 1, 1989, pp. 19-84.; R. Backhouse, P. Chisholm, G. Malcom, E. Saaman, Do-it-yourself Type Theory, Formal Aspects of Computing, vol. 1, 1989, pp. 19-84. · Zbl 0697.68020 |
| [2] | Barendregt, H., The Lambda Calculus, its Syntax and Semantics, Studies in Logic and Foundations of Mathematics (1984), North-Holland: North-Holland Amsterdam · Zbl 0551.03007 |
| [3] | Maietti, M. E., About effective quotients in constructive type theory, (Altenkirch, T.; Naraschewski, W.; Reus, B., Types for Proofs and Programs, International Workshop “Types’98”. Types for Proofs and Programs, International Workshop “Types’98”, Lecture Notes in Computer Science, vol. 1657 (1999), Springer: Springer Berlin), 164-178 · Zbl 0943.03053 |
| [4] | Martin-Löf, P., Intuitionistic Type Theory, notes by G. Sambin of a series of lectures given in Padua (1984), Bibliopolis: Bibliopolis Naples · Zbl 0571.03030 |
| [5] | Nordström, B.; Peterson, K.; Smith, J., Programming in Martin-Löf’s Type Theory, An introduction (1990), Clarendon Press: Clarendon Press Oxford · Zbl 0744.03029 |
| [6] | Sambin, G., Intuitionistic formal spaces—a first communication, (Skordev, D., Mathematical Logic and its Applications (1987), Plenum Press: Plenum Press New York), 187-204 · Zbl 0703.03040 |
| [7] | Sambin, G.; Valentini, S., Building up a tool-box for Martin-Löf intuitionistic type theory, (Sambin, G.; Smith, J., Twenty-five Years of Constructive Type Theory. Twenty-five Years of Constructive Type Theory, Oxford Logic Guides, vol. 36 (1998), Oxford University Press: Oxford University Press New York), 221-244 · Zbl 0930.03091 |
| [8] | Sambin, G.; Valentini, S.; Virgili, P., Constructive domain theory as a branch of Intuitionistic Pointfree Topology, Theoret. Comput. Sci., 159, 319-341 (1996) · Zbl 0871.68063 |
| [9] | D.S. Scott, Lectures on a mathematical theory of computation, Oxford University Computing Laboratory Technical Monograph PRG-19, 1981.; D.S. Scott, Lectures on a mathematical theory of computation, Oxford University Computing Laboratory Technical Monograph PRG-19, 1981. |
| [10] | Scott, D. S., Domains for denotational semantics, (Nielsen, M.; Schmidt, E. M., Automata, Languages and Programming (1982), Springer: Springer Berlin), 577-613 · Zbl 0495.68025 |
| [11] | Valentini, S., Decidability in Intuitionistic Theory of Types is functionally decidable, Math. Logic Quart., 42, 300-304 (1996) · Zbl 0854.03008 |
| [12] | Valentini, S., Extensionality versus Constructivity, Mathematical Logic Quart., 48, 2, 179-187 (2002) · Zbl 0997.03047 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
