Lambda the Ultimate

A Mobility Calculus with Local and Dependent Types, by Mario Coppo, Federico Cozzi, Mariangiola Dezani-Ciancaglini, Elio Giovannetti and Rosario Pugliese

Abstract:

We introduce an ambient calculus that combines ambient mobility with process mobility, uses group names to group ambients with homologous features, and exploits co-moves and runtime type checking to implement flexible policies for controlling process activities. Types rely on group names and, to support dynamicity, may depend on group variables. Policies can dynamically change also through installation of co-moves. The compliance with ambient policies can be checked locally to the ambients and requires no global assumptions. We prove that the type assignment system and the operational semantics of the calculus are ‘sound’, and we define a sound and complete type inference algorithm which, when applied to terms whose type decorations only express the desired policies, computes the minimal type annotations required for their execution.
As an application of our calculus, we present a couple of examples and linger on the setting up of policies for controlling the activities of the objects involved.

The Charles Babbage Institute is an historical archives and research center of the University of Minnesota. CBI is dedicated to promoting study of the history of information technology and information processing and their impact on society. CBI preserves relevant historical documentation in all media, conducts and fosters research in history and archival methods, offers graduate fellowships, and sponsors symposia, conferences, and publications.

Mission

CBI historians design and administer research projects in the history of information technology and engage in original research that is disseminated through scholarly publications, conference presentations, and the CBI web site. CBI archivists collect, preserve, and make available for research primary source materials relating to the history of information technology. The archival collection consists of corporate records, manuscript materials, records of professional associations, oral history interviews, trade publications, periodicals, obsolete manuals and product literature, photographs, films, videos, and reference materials. CBI also serves as a clearinghouse for resources on the history of information technology.

(Copied from the "about section" of the CBI site, hope that is allowed)

Didn't find any reference to this site on Ltu. Guess it might be of interest to the history department.