[PRL] Fwd: [MIT-PL] PL Seminar on Monday: Hongwei Xi on the ATS language

[Sam Tobin-Hochstadt]

This looks potentially interesting to many PRL folks.

---------- Forwarded message ----------
From: Adam Chlipala <adamc at csail.mit.edu>
Date: Thu, Dec 1, 2011 at 8:36 AM
Subject: [MIT-PL] PL Seminar on Monday: Hongwei Xi on the ATS language
To: pl at lists.csail.mit.edu


Date: December 5
Time: 4:00-5:30
Room: 32-D463 (Star)

Speaker: Hongwei Xi <http://www.cs.bu.edu/~hwxi/>, Boston University

Title: Views and Viewtypes in ATS

ATS is a statically typed general-purpose programming language.  The
signatory feature of ATS is a programming paradigm named
programming-with-theorem-proving in which code for (run-time)
computation and code for proof construction can be written in a
syntactically intertwined manner.  In ATS, there is direct support for
both dependent types and linear types. While the dependent types in
ATS, which are of a restricted form originated from the development of
Dependent ML (DML), are well-studied, the linear types in ATS are much
less well-known.  In this talk, I will give an introduction to a
notion of linear types referred to as viewtypes in ATS, which combine
views (i.e., linear types for proofs) and types (for run-time values).
In addition, I will present several concrete examples to illustrate
certain practical uses of views and viewtypes.

_______________________________________________
Pl mailing list
Pl at lists.csail.mit.edu
https://lists.csail.mit.edu/mailman/listinfo/pl
http://projects.csail.mit.edu/pl


-- 
sam th
samth at ccs.neu.edu