Constructive sheaf semantics

被引:8
|
作者
Palmgren, E [1 ]
机构
[1] UNIV UPPSALA,DEPT MATH,S-75106 UPPSALA,SWEDEN
关键词
constructive model theory; sheaf semantics; intuitionistic logic; completeness;
D O I
10.1002/malq.19970430304
中图分类号
O1 [数学];
学科分类号
0701 ; 070101 ;
摘要
Sheaf semantics is developed within a constructive and predicative framework, Martin-Lof's type theory. We prove strong completeness of many sorted, first order intuitionistic logic with respect to this semantics, by using sites of provably functional relations.
引用
收藏
页码:321 / 327
页数:7
相关论文
共 50 条
  • [1] A SHEAF SEMANTICS FOR FOOPS EXPRESSIONS
    WOLFRAM, DA
    GOGUEN, JA
    [J]. LECTURE NOTES IN COMPUTER SCIENCE, 1992, 612 : 81 - 98
  • [2] Constructive sheaf models of type theory
    Coquand, Thierry
    Ruch, Fabian
    Sattler, Christian
    [J]. MATHEMATICAL STRUCTURES IN COMPUTER SCIENCE, 2021, 31 (09) : 979 - 1002
  • [3] Towards a sheaf semantics for cooperating agents scenarios
    Sofronie, V.
    [J]. Lecture Notes in Computer Science, 1996, 1138
  • [4] Constructive action semantics in OBJ
    Mosses, Peter D.
    [J]. ALGEBRA, MEANING, AND COMPUTATION: ESSAYS DEDICATED TO JOSEPH A. GOGUEN ON THE OCCASION OF HIS 65TH BIRTHDAY, 2006, 4060 : 281 - 295
  • [5] Explicit provability and constructive semantics
    Artemov, SN
    [J]. BULLETIN OF SYMBOLIC LOGIC, 2001, 7 (01) : 1 - 36
  • [6] Constructive semantics for extensional PTQ
    Pérez, RD
    [J]. PROCEEDINGS OF THE FOURTH MEXICAN INTERNATIONAL CONFERENCE ON COMPUTER SCIENCE (ENC 2003), 2003, : 33 - 39
  • [7] Constructive semantics for instantaneous reactions
    Aguado, Joaquin
    Mendler, Michael
    [J]. THEORETICAL COMPUTER SCIENCE, 2011, 412 (11) : 931 - 961
  • [8] ON CONNECTIONS BETWEEN CLASSICAL AND CONSTRUCTIVE SEMANTICS
    STARCHENKO, SS
    VORONKOV, AA
    [J]. LECTURE NOTES IN COMPUTER SCIENCE, 1990, 417 : 275 - 285
  • [9] CONNECTING FORMAL SEMANTICS TO CONSTRUCTIVE INTUITIONS
    KURTZ, SA
    MITCHELL, JC
    ODONNELL, MJ
    [J]. LECTURE NOTES IN COMPUTER SCIENCE, 1992, 613 : 1 - 21
  • [10] Game Semantics for Constructive Modal Logic
    Acclavio, Matteo
    Catta, Davide
    Strassburger, Lutz
    [J]. AUTOMATED REASONING WITH ANALYTIC TABLEAUX AND RELATED METHODS, TABLEAUX 2021, 2021, 12842 : 428 - 445