Programmers and software engineers agree in unanimity that a useful characteristic of the programming languages they use for implementations (C++, Java, etc.) is their support for both public and private features (types, functions). The public features are often called interfaces. The private part is not visible outside the module (class, package) that declares it, but it can be used internally to define the visible part. Such distinction helps software engineers abstract their work and ignore details which are a main source of confusion and errors. We claim that the distinction between private and public features might also be a desirable characteristic of formal specifications, not only from the practical point of view but also because of at least two important theoretical reasons. One is the possibility to finitely specify theories which do not admit finite standard presentations. For example, Bergstra and Tucker showed that any recursive algebra is a restriction of an initial algebra presented by a finite number of equations over a larger signature. Another reason is that it allows the user to specify behavioral properties of systems, in the sense that every behavioral specification is equivalent to hiding some operators (i.e., making them private) in a usual specification. We introduce the notion of module specification as a generalization of the standard specification, having both public (or visible) and private features, and then explore their properties at an abstract level, categorical. To formalize the notion of ``logical system'' we use {\em institutions} enriched with inclusions, an abstraction of the natural notion of inclusion of signatures from particular logics. The visible theorems (or the visible consequences) of a module are those theorems which contain only visible symbols, and a model of that module is a model of its visible consequences. Five basic operations on module specifications are explored: renaming, hiding, enriching, aggregation and parameterization. An internal property of modules, conservativeness, seems to have a decisive role in giving semantics for module composition.

Pre-2018 CSE ID: CS2000-0653

Proof-carrying code is a technique that can be used to execute untrusted code safely. A code consumer specifies requirements and safety rules which define the safe behavior of a system, and a code producer packages each program with a formal proof that the program satisfies the requirements. The consumer uses a fast proof validator to check that the proof is correct, and hence the program is safe. In this report, we discuss applications for which proof-carrying code is appropriate, explain the mechanics of proof-carrying code, compare it with other security techniques and propose research directions for the method.

Pre-2018 CSE ID: CS1999-0633

Circular coinduction is a new technique for behavioral reasoning that extends coinduction to specifications with circularities. We show that a congruence criterion due to Bidoit and Hennicker follows easily from circular coinduction, and we give some natural examples of circular coinductive proofs. A notation, called BOBJ, appropriate for our style of behavioral specification is also sketched. Finally, everything is conducted in a general framework that in a sense is the gcd of previous behavioral frameworks.

Pre-2018 CSE ID: CS2000-0647