Lambda the Ultimate

Universal Temporal Concurrent Constraint Programming (full text available)

Olarte, Carlos (2009) Universal Temporal Concurrent Constraint Programming. PhD thesis Informatique, LIX, EP/X p.167.

Concurrent Constraint Programming (CCP) is a formalism for concurrency in which agents (processes) interact with one another by telling (adding) and asking (reading) information represented as constraints in a shared medium (the store). Temporal Concurrent Constraint Programming (tcc) extends CCP by allowing agents to be constrained by time conditions. This dissertation studies temporal CCP as a model of concurrency for mobile, timed reactive systems. The study is conducted by developing a process calculus called utcc, Universal Temporal CCP. The thesis is that utcc is a model for concurrency where behavioral and declarative reasoning techniques coexist coherently, thus allowing for the specification and verification of mobile reactive systems in emergent application areas.

The utcc calculus generalizes tcc, a temporal CCP model of reactive synchronous programming, with the ability to express mobility. Here mobility is understood as communication of private names as typically done for mobile systems and security protocols. The utcc calculus introduces parametric ask operations called abstractions that behave as persistent parametric asks during a time-interval but may disappear afterwards. The applicability of the calculus is shown in several domains of Computer Science. Namely, decidability of Pnueli's First-order Temporal Logic, closure-operator semantic characterization of security protocols, semantics of a Service-Oriented Computing language, and modeling of Dynamic Multimedia-Interaction systems.

(emphasis mine)

I came across this while developing a capability-secure fusion of constraint programming and reactive programming. It seems UTCC achieves properties similar or identical to those I am pursuing, such as effective support for security, live programming, and interactive multi-media. I'll say more when I stop reading the thesis.

Eiffel in its current form is not completely type safe. One kind of type error is possible. It is called catcall in Eiffel speak. The compiler cannot detect this kind of type error. A catcall usually triggers an exception at runtime.

This type error is possible due to covariant redefinition of arguments and polymorphy (i.e. subtyping). Both principles are very powerful in OO programming. Other languagues (like java, scala, etc.) solve this problem by disallowing covariant redefinitions of arguments and keeping polymorphy (subtyping).

Since both, covariant redefinition of arguments and polymorphy, add a lot of power to object oriented programming, a solution to the catcall problem shall keep both, covariance and polymorphy, and rule out the potential type errors.

This paper introduces a solution to the catcall problem by imposing stricter rules and making inheritance more fine granular by keeping the expressiveness of the language.

Read the detailed paper at http://tecomp.sourceforge.net -> White papers -> Language discussion -> Solution to the catcall problem.