Home Online Resources Table of Contents

Journal of Logic and Computation, Volume 8, Issue 1: February 1998.

A module system for a programming language based on the LF logical framework

R Harper and F Pfenning

School of Computer Science, Carnegie Mellon University, Pittsburgh, Pennsylvania 15213-3890, USA. E-mail: rwh+@cs.cmu.edu andfp+@cs.cmu.edu

We describe a module system for Elf, a logic programming language based on the LF logical framework. The static part of the module calculus addresses name-space management and structured presentation of deductive systems. The dynamic part addresses search-space management and modularization of logic programs.

Keywords: Logical frameworks, typed [lgr]-calculus, dependent types, modularity, structured theories, logic programming.

Pages 5-31


This page is run by Oxford University Press, Great Clarendon Street, Oxford OX2 6DP, UK
as part of the OUP Journals World Wide Web service.
Comments and feedback: www-admin@oup.co.uk
URL: http://www.oup.co.uk/logcom/hdb/Volume_08/Issue_01/080005.sgm.abs.html
Last modification: 1 June 1998.
Copyright© Oxford University Press, 1998.