Coercive Subtyping in Lambda-Free Logical Frameworks

Robin Adams

doi:10.1145/1577824.1577830

Coercive Subtyping in Lambda-Free Logical Frameworks

Robin Adams

Department of Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

36 Downloads (Pure)

Abstract

We show how coercive subtyping may be added to a lambda-free logical framework, by constructing the logical framework TF<, an extension of the lambda-free logical framework TF with coercive subtyping. Instead of coercive application, TF< makes use of a typecasting operation. We develop the metatheory of the resulting framework, including providing some general conditions under which typecasting in an object theory with coercive subtyping is decidable. We show how TF< may be embedded in the logical framework LF, and hence how results about LF may be deduced from results about TF<

Original language	English
Title of host publication	Proceedings of the Fourth international Workshop on Logical Frameworks and Meta-Languages
Editors	James Cheney, Amy Felty
Place of Publication	New York
Publisher	ACM
Pages	30-39
Number of pages	10
ISBN (Print)	978-1-60558-529-1
DOIs	https://doi.org/10.1145/1577824.1577830
Publication status	Published - 2009
Event	LFMTP'09 - Montreal, Canada Duration: 2 Aug 2009 → 2 Aug 2009

Publication series

Name
Publisher	ACM

Conference

Conference	LFMTP'09
Country/Territory	Canada
City	Montreal
Period	2/08/09 → 2/08/09

Keywords

coercive subtyping
type theory
canonical logical framework
typecasting
metatheory

Access to Document

10.1145/1577824.1577830

Reverse Mathematics in Dependent Type Theory
Adams, R. (PI)
Eng & Phys Sci Res Council EPSRC
16/10/06 → 15/09/09
Project: Research

Cite this

@inproceedings{8b34219c5f00425bbfeab23239d0b9b3,

title = "Coercive Subtyping in Lambda-Free Logical Frameworks",

abstract = "We show how coercive subtyping may be added to a lambda-free logical framework, by constructing the logical framework TF<, an extension of the lambda-free logical framework TF with coercive subtyping. Instead of coercive application, TF< makes use of a typecasting operation. We develop the metatheory of the resulting framework, including providing some general conditions under which typecasting in an object theory with coercive subtyping is decidable. We show how TF< may be embedded in the logical framework LF, and hence how results about LF may be deduced from results about TF<",

keywords = "coercive subtyping, type theory, canonical logical framework, typecasting, metatheory",

author = "Robin Adams",

year = "2009",

doi = "10.1145/1577824.1577830",

language = "English",

isbn = "978-1-60558-529-1 ",

publisher = "ACM",

pages = "30--39",

editor = "James Cheney and Amy Felty",

booktitle = "Proceedings of the Fourth international Workshop on Logical Frameworks and Meta-Languages",

note = "LFMTP'09 ; Conference date: 02-08-2009 Through 02-08-2009",

}

TY - GEN

T1 - Coercive Subtyping in Lambda-Free Logical Frameworks

AU - Adams, Robin

PY - 2009

Y1 - 2009

N2 - We show how coercive subtyping may be added to a lambda-free logical framework, by constructing the logical framework TF<, an extension of the lambda-free logical framework TF with coercive subtyping. Instead of coercive application, TF< makes use of a typecasting operation. We develop the metatheory of the resulting framework, including providing some general conditions under which typecasting in an object theory with coercive subtyping is decidable. We show how TF< may be embedded in the logical framework LF, and hence how results about LF may be deduced from results about TF<

AB - We show how coercive subtyping may be added to a lambda-free logical framework, by constructing the logical framework TF<, an extension of the lambda-free logical framework TF with coercive subtyping. Instead of coercive application, TF< makes use of a typecasting operation. We develop the metatheory of the resulting framework, including providing some general conditions under which typecasting in an object theory with coercive subtyping is decidable. We show how TF< may be embedded in the logical framework LF, and hence how results about LF may be deduced from results about TF<

KW - coercive subtyping

KW - type theory

KW - canonical logical framework

KW - typecasting

KW - metatheory

U2 - 10.1145/1577824.1577830

DO - 10.1145/1577824.1577830

M3 - Conference contribution

SN - 978-1-60558-529-1

SP - 30

EP - 39

BT - Proceedings of the Fourth international Workshop on Logical Frameworks and Meta-Languages

A2 - Cheney, James

A2 - Felty, Amy

PB - ACM

CY - New York

T2 - LFMTP'09

Y2 - 2 August 2009 through 2 August 2009

ER -

Coercive Subtyping in Lambda-Free Logical Frameworks

Abstract

Publication series

Conference

Keywords

Access to Document

Projects

Reverse Mathematics in Dependent Type Theory

Cite this