Search

The ML module system provides powerful parameterization facilities, but lacks the ability to split mutually recursive definitions across modules and provides insufficient support for incremental programming. A promising approach to solve these issues is Ancona and Zucca's mixin module calculus CMS. However, the straightforward way to adapt it to ML fails, because it allows arbitrary recursive definitions to appear at any time, which ML does not otherwise support. In this article, we enrich CMS with a refined type system that controls recursive definitions through the use of dependency graphs. We then develop and prove sound a separate compilation scheme, directed by dependency graphs, that translates mixin modules down to a call-by-value [lambda]-calculus extended with a nonstandard 1et rec construct. Categories and Subject Descriptors: D.3.1 [Programming Languages]: Formal Definitions and Theory--Semantics; D.3.2 [Programming Languages]: Language Classifications--Applicative (functional) languages; object-oriented languages; D.3.3 [Programming Languages]: Language Constructs and Features Inheritance;modules;packages;recursion;F.3.2[LogicsandMeanings of Programs]: Semantics of Programming Languages--Operational semantics; F.3.3 [Logics and Meanings of Programs]: Studies of Program Constructs--Type structure General Terms: Languages, Theory Additional Key Words and Phrases: Mixins, modules, recursion, type systems

In programming language and software engineering, the main mathematical tool is de facto some form of predicate logic. Yet, as elsewhere in applied mathematics, it is used mostly far below its potential, due to its traditional formulation as just a topic in logic instead of a calculus for everyday practical use. The proposed alternative combines a language of utmost simplicity (four constructs only) that is devoid of the defects of common mathematical conventions, with a set of convenient calculation rules that is sufficiently comprehensive to make it practical for everyday use in most (if not all) domains of interest. Its main elements are a functional predicate calculus and concrete generic functionals. The first supports formal calculation with quantifiers with the same fluency as with derivatives and integrals in classical applied mathematics and engineering. The second achieves the same for calculating with functionals, including smooth transition between pointwise and point-free expression. The extensive collection of examples pertains mainly to software specification, language semantics and its mathematical basis, program calculation etc., but occasionally shows wider applicability throughout applied mathematics and engineering. Often it illustrates how formal reasoning guided by the shape of the expressions is an instrument for discovery and expanding intuition, or highlights design opportunities in declarative and (functional) programming languages. Categories and Subject Descriptors: D.2.1 [Software Engineering]: Requirements/Specifications; D.3.1 [Programming Languages]: Formal Definition and Theory; E.1 [Data Structures]; F.4.1 [Mathematical Logic and Formal Languages]: Mathematical Logic; F.4.3 [Mathematical Logic and Formal Languages]: Formal Languages; I.l.1 [Symbolic and Algebraic Manipulation]: Expressions and Their Representation; I. 1.3 [Symbolic and Algebraic Manipulation]: Languages and Systems; K.3.2 [Computers and Eduction]: Computer and Information Science Education General Terms: Design, Documentation, Languages, Theory, Verification Additional Key Words and Phrases: Analysis, binary algebra, calculational reasoning, databases, declarative languages, elastic operators, function equality, functional predicate calculus, generic functionals, Leibniz's principle, limits, programming languages, program semantics, quantifiers, recursion, software engineering, summation