|
Hongwei Xi
Applied type system (extended
abstract)
In post-workshop Proceedings of TYPES 2003, pages 394-408
Springer-Verlag LNCS 3085, 2004
The framework Pure Type System (PTS) offers a simple and general
approach to designing and formalizing type systems. However, in the
presence of dependent types, there often exist some acute problems that
make it difficult for PTS to accommodate many common realistic
programming features such as general recursion, recursive types, effects
(e.g., exceptions, references, input/output), etc. In this paper, we
propose a new framework Applied Type System (ATS) to allow for designing
and formalizing type systems that can readily support common realistic
programming features. The key salient feature of ATS lies in a complete
separation between statics, in which types are formed and reasoned about,
and dynamics, in which programs are constructed and evaluated. With this
separation, it is no longer possible for a program to occur in a type as is
otherwise allowed in PTS. We present not only a formal development of
ATS but also mention some examples in support of using ATS as a
framework to form type systems for practical programming.
[ bib |
.ps |
.pdf ]
Back
This file has been generated by
bibtex2html 1.61
Copyright notice: The documents contained
in these pages are included by the contributing authors as a means to
ensure timely dissemination of scholarly and technical work on a
non-commercial basis. Copyright and all rights therein are maintained
by the authors or by other copyright holders, notwithstanding that
they have offered their works here electronically. It is understood that all persons copying this information will
adhere to the terms and constraints invoked by each author's
copyright. These works
may not be reposted without the explicit permission of the copyright
holder.
If you experience problems downloading any of the files above,
it is most likely because your browser does not handle compressed
files correctly.
In particular, Netscape might save the file in the compressed
gz-format with extension .ps or
.pdf (indicating postscript or PDF, resp.). You can work around this by saving the file,
renaming it to .ps.gz or .pdf.gz, and then
uncrompress it.
|
