Coercive Subtyping in Lambda-Free Logical Frameworks

Robin Adams

Research output: Chapter in Book/Report/Conference proceedingConference 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 languageEnglish
Title of host publicationProceedings of the Fourth international Workshop on Logical Frameworks and Meta-Languages
EditorsJames Cheney, Amy Felty
Place of PublicationNew York
PublisherACM
Pages30-39
Number of pages10
ISBN (Print)978-1-60558-529-1
DOIs
Publication statusPublished - 2009
EventLFMTP'09 - Montreal, Canada
Duration: 2 Aug 20092 Aug 2009

Publication series

Name
PublisherACM

Conference

ConferenceLFMTP'09
Country/TerritoryCanada
CityMontreal
Period2/08/092/08/09

Keywords

  • coercive subtyping
  • type theory
  • canonical logical framework
  • typecasting
  • metatheory

Cite this