Constructive canonicity for lattice-based fixed point logics

Willem Conradie, Andrew Craig, Alessandra Palmigiano, Zhiguang Zhao

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

10 Citations (Scopus)

Abstract

In the present paper, we prove canonicity results for lattice-based fixed point logics in a constructive meta-theory. Specifically, we prove two types of canonicity results, depending on how the fixed-point binders are interpreted. These results smoothly unify the constructive canonicity results for inductive inequalities, proved in a general lattice setting, with the canonicity results for fixed point logics on a bi-intuitionistic base, proven in a non-constructive setting.

Original languageEnglish
Title of host publicationLogic, Language, Information, and Computation - 24th International Workshop, WoLLIC 2017, Proceedings
EditorsJuliette Kennedy, Ruy J.G.B. de Queiroz
PublisherSpringer Verlag
Pages92-109
Number of pages18
ISBN (Print)9783662553855
DOIs
Publication statusPublished - 2017
Event24th International Workshop on Logic, Language, Information, and Computation, WoLLIC 2017 - London, United Kingdom
Duration: 18 Jul 201721 Jul 2017

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume10388 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference24th International Workshop on Logic, Language, Information, and Computation, WoLLIC 2017
Country/TerritoryUnited Kingdom
CityLondon
Period18/07/1721/07/17

Keywords

  • Canonicity
  • Lattice-based fixed point logics
  • Logics for categorization
  • Unified correspondence

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science

Fingerprint

Dive into the research topics of 'Constructive canonicity for lattice-based fixed point logics'. Together they form a unique fingerprint.

Cite this