Categorical models of explicit substitutions

被引：0
|
作者：
Ghani, N [1 ]
de Paiva, V [1 ]
Ritter, E [1 ]
机构：
[1] Univ Birmingham, Birmingham B15 2TT, W Midlands, England
来源：
FOUNDATIONS OF SOFTWARE SCIENCE AND COMPUTATION STRUCTURES | 1999年 / 1578卷
关键词：
D O I：
暂无
中图分类号：
TP31 [计算机软件];
学科分类号：
081202 ; 0835 ;
摘要：
Indexed categories provide models of cartesian calculi of explicit substitutions. However, these structures are inherently non-linear and hence cannot be used to model linear calculi of explicit substitution. This paper replaces indexed categories with pre-sheaves, thus providing a categorical semantics covering both the linear and cartesian cases. We further justify our models by proving soundness and completeness results.
引用
收藏
页码：197 / 211
页数：15
相关论文
共 50 条
  • [1] On explicit substitutions and names
    Ritter, E
    de Paiva, V
    [J]. AUTOMATA, LANGUAGES AND PROGRAMMING, 1997, 1256 : 248 - 258
  • [2] Combinatorics of Explicit Substitutions
    Bendkowski, Maciej
    Lescanne, Pierre
    [J]. PPDP'18: PROCEEDINGS OF THE 20TH INTERNATIONAL SYMPOSIUM ON PRINCIPLES AND PRACTICE OF DECLARATIVE PROGRAMMING, 2018,
  • [3] Explicit substitutions and reducibility
    Herbelin, H
    [J]. JOURNAL OF LOGIC AND COMPUTATION, 2001, 11 (03) : 431 - 451
  • [4] Intersection types for explicit substitutions
    Lengrand, S
    Lescanne, P
    Dougherty, D
    Dezani-Ciancaglini, M
    van Bakel, S
    [J]. INFORMATION AND COMPUTATION, 2004, 189 (01) : 17 - 42
  • [5] Functional programming and explicit substitutions
    Lescanne, P
    [J]. CARI'96 - PROCEEDINGS OF THE 3RD AFRICAN CONFERENCE ON RESEARCH IN COMPUTER SCIENCE, 1996, : 830 - 841
  • [6] Explicit Substitutions: A Short Survey
    Pierre-LoutsCurien
    [J]. Journal of Computer Science & Technology, 1998, (06) : 562 - 563
  • [7] On a logical foundation for explicit substitutions
    Pfenning, Frank
    [J]. Typed Lambda Calculi and Applications, Proceedings, 2007, 4583 : 1 - 1
  • [8] Logic of predicates with explicit substitutions
    Bednarczyk, MA
    [J]. MATHEMATICAL FOUNDATIONS OF COMPUTER SCIENCE 1996, 1996, 1113 : 192 - 205
  • [9] A COMPLETENESS RESULT FOR EXPLICIT SUBSTITUTIONS
    CURIEN, PL
    RIOS, A
    [J]. COMPTES RENDUS DE L ACADEMIE DES SCIENCES SERIE I-MATHEMATIQUE, 1991, 312 (06): : 471 - 476
  • [10] Proof nets and explicit substitutions
    Di Cosmo, R
    Kesner, D
    Polonovski, E
    [J]. FOUNDATIONS OF SOFTWARE SCIENCE AND COMPUTATION STRUCTURES, 2000, 1784 : 63 - 81
12345