1 Search Results for "Ko, Hsiang-Shang"

Document

DOI: 10.4230/LIPIcs.CSL.2022.14

Realising Intensional S4 and GL Modalities

Authors: Liang-Ting Chen and Hsiang-Shang Ko

Published in: LIPIcs, Volume 216, 30th EACSL Annual Conference on Computer Science Logic (CSL 2022)

Abstract

There have been investigations into type-theoretic foundations for metaprogramming, notably Davies and Pfenning’s (2001) treatment in S4 modal logic, where code evaluating to values of type A is given the modal type Code A (□A in the original paper). Recently Kavvos (2017) extended PCF with Code A and intensional recursion, understood as the deductive form of the GL (Gödel-Löb) axiom in provability logic, but the resulting type system is logically inconsistent. Inspired by staged computation, we observe that a term of type Code A is, in general, code to be evaluated in a next stage, whereas S4 modal type theory is a special case where code can be evaluated in the current stage, and the two types of code should be discriminated. Consequently, we use two separate modalities ⊠ and □ to model S4 and GL respectively in a unified categorical framework while retaining logical consistency. Following Kavvos’ (2017) novel approach to the semantics of intensionality, we interpret the two modalities in the P-category of assemblies and trackable maps. For the GL modality □ in particular, we use guarded type theory to articulate what it means by a “next” stage and to model intensional recursion by guarded recursion together with Kleene’s second recursion theorem. Besides validating the S4 and GL axioms, our model better captures the essence of intensionality by refuting congruence (so that two extensionally equal terms may not be intensionally equal) and internal quoting (both A → □A and A → ⊠A). Our results are developed in (guarded) homotopy type theory and formalised in Agda.

Cite as

Liang-Ting Chen and Hsiang-Shang Ko. Realising Intensional S4 and GL Modalities. In 30th EACSL Annual Conference on Computer Science Logic (CSL 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 216, pp. 14:1-14:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{chen_et_al:LIPIcs.CSL.2022.14,
  author =	{Chen, Liang-Ting and Ko, Hsiang-Shang},
  title =	{{Realising Intensional S4 and GL Modalities}},
  booktitle =	{30th EACSL Annual Conference on Computer Science Logic (CSL 2022)},
  pages =	{14:1--14:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-218-1},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{216},
  editor =	{Manea, Florin and Simpson, Alex},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2022.14},
  URN =		{urn:nbn:de:0030-drops-157341},
  doi =		{10.4230/LIPIcs.CSL.2022.14},
  annote =	{Keywords: provability, guarded recursion, realisability, modal types, metaprogramming}
}

Refine by Author
1 Chen, Liang-Ting
1 Ko, Hsiang-Shang

Refine by Classification
1 Theory of computation → Type theory

Refine by Keyword
1 guarded recursion
1 metaprogramming
1 modal types
1 provability
1 realisability

Refine by Type
1 document

Refine by Publication Year
1 2022

1 Search Results for "Ko, Hsiang-Shang"

Realising Intensional S4 and GL Modalities

Abstract

Cite as

Thanks for your feedback!

Could not send message