Normalization for Cubical Type Theory

被引：10
|
作者：
Sterling, Jonathan [1 ]
Angiuli, Carlo [1 ]
机构：
[1] Carnegie Mellon Univ, Comp Sci Dept, Pittsburgh, PA 15213 USA
来源：
2021 36TH ANNUAL ACM/IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE (LICS) | 2021年
关键词：
1ST STEPS;
D O I：
10.1109/LICS52264.2021.9470719
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
We prove normalization for (univalent, Cartesian) cubical type theory, closing the last major open problem in the syntactic metatheory of cubical type theory. Our normalization result is reduction-free, in the sense of yielding a bijection between equivalence classes of terms in context and a tractable language of beta/eta-normal forms. As corollaries we obtain both decidability of judgmental equality and the injectivity of type constructors.
引用
收藏
页数：15
相关论文
共 50 条
  • [41] The normalization group in quantum theory
    Petermann, A.
    E.C.G. STUECKELBERG, AN UNCONVENTIONAL FIGURE OF TWENTIETH CENTURY PHYSICS, 2009, : 395 - 398
  • [42] BASIC THEORY ON NORMALIZATION OF PATTERN
    IJIMA, T
    IEEE TRANSACTIONS ON INFORMATION THEORY, 1964, 10 (04) : 402 - &
  • [43] CUBICAL GRAPHS AND CUBICAL DIMENSIONS.
    Harary, Frank
    Computers & mathematics with applications, 1986, 15 (04): : 271 - 275
  • [44] Normalization of ZZ instanton amplitudes in type 0B minimal superstring theory
    Chakrabhavi, Vivek
    Eniceicu, Dan Stefan
    Mahajan, Raghu
    Murdia, Chitraang
    JOURNAL OF HIGH ENERGY PHYSICS, 2024, (09):
  • [45] KAROUBI-VILLAMAYOR K-THEORY OF CUBICAL RINGS
    DAYTON, B
    NOTICES OF THE AMERICAN MATHEMATICAL SOCIETY, 1976, 23 (06): : A611 - A612
  • [46] Development of a theory of implementation and integration: Normalization Process Theory
    Carl R May
    Frances Mair
    Tracy Finch
    Anne MacFarlane
    Christopher Dowrick
    Shaun Treweek
    Tim Rapley
    Luciana Ballini
    Bie Nio Ong
    Anne Rogers
    Elizabeth Murray
    Glyn Elwyn
    France Légaré
    Jane Gunn
    Victor M Montori
    Implementation Science, 4
  • [47] Development of a theory of implementation and integration: Normalization Process Theory
    May, Carl R.
    Mair, Frances
    Finch, Tracy
    MacFarlane, Anne
    Dowrick, Christopher
    Treweek, Shaun
    Rapley, Tim
    Ballini, Luciana
    Ong, Bie Nio
    Rogers, Anne
    Murray, Elizabeth
    Elwyn, Glyn
    Legare, France
    Gunn, Jane
    Montori, Victor M.
    IMPLEMENTATION SCIENCE, 2009, 4
  • [48] A new universal real flow of the Hilbert-cubical type
    Jin, Lei
    Tu, Siming
    DYNAMICAL SYSTEMS-AN INTERNATIONAL JOURNAL, 2019, 34 (02): : 234 - 238
  • [49] Normalization of D instanton amplitudes in two dimensional type 0B string theory
    Joydeep Chakravarty
    Ashoke Sen
    Journal of High Energy Physics, 2023
  • [50] Normalization of D instanton amplitudes in two dimensional type 0B string theory
    Chakravarty, Joydeep
    Sen, Ashoke
    JOURNAL OF HIGH ENERGY PHYSICS, 2023, 2023 (02)
12345