Talks from 2006/2007

26th July 2007 Towards a formal language for writing electronic contracts (Gerardo Schneider) Abstract: In this talk I will describe CL, a language for writing (electronic) contracts with semantics in an extension of the mu-calculus. The language allows to write (conditional) obligations, permissions and prohibitions, and to represent the so-called contrary-to-duty (CTD) and contrary-to-prohibition (CTP). CTDs and CTPs are useful to establish what happens in case an obligation, respectively a prohibition, is not respected. The approach is action-based, meaning that the above normative notions are defined on actions and not on state-of-affairs. I will then describe the main limitations of the language, and sketch some initial work on model checking contracts. I will also describe research directions we intend to pursue, including extensions of the language with timing constraints, and further development of theoretical foundations to analyse contracts. 26th June 2007 reFLect - A functional language with reflection features (Christian Tabone) Abstract: Consider using a functional language to embed a simple Hardware Description Language, and consequently dealing with the choice of either opting for a shallow embedding approach or a deep embedding approach. Deeply embedding an HDL is usually preferred since it provides a form of control over the structure of the defined circuits, which is not available when choosing a shallow embedding. On the other hand, a shallow embedding of an HDL is more natural to use and understand, offering the evaluation features of the host language available in the HDL. In this talk we present reFLect as a functional language with reflection features which provides an alternative approach for embedding a hardware description language. By using quotation and antiquotation constructs over defined expressions, reFLect offers an environment where the power of deep embedding is made available as a shallow embedding. 8th March 2007 Embedded Languages in the Functional Paradigm (Joseph Cordina) Abstract: Whenever one requires added functionality to meet the demands of a particular problem domain, either a new programming language is designed or a library is provided that can be reused by a particular programming language. An embedded language is the combination of both these solutions, providing the programmer with the benefits of both approaches. In this first of a series of talks, an introduction to embedded languages will be given and a series of typical problems will highlighted. In subsequent talks, a number of solutions will be analysed. We will be highlighting the use of functional programming for writing embedded languages due to the large number of advantages this paradigm provides (most importantly referential transparency and functional composition). As an example problem domain, we will discuss how to construct an embedded language for describing and manipulating digital circuits. 19th February 2007 Context-Sensitive Parser Combinators (Gordon Pace) Abstract: Combinator-based parsing using functional programming provides an elegant, and compositional approach to parser design and development. By its very nature, sensitivity to context usually fails to be properly addressed in these approaches. In this talk, we will identify two techniques to deal with context compositionally, particularly suited for natural language parsing. To enable efficient and compositional parsing, we will show how standard monadic parser combinators can be modified to deal with reverse parsing. As case studies, we will show how these new combinators can be used to parse Maltese definite nouns and conjugated verbs of the first form. 15th January 2007 Interface Refinements (Sandro Spina) Abstract: Interfaces define the behavioural restrictions imposed on a particular process by synchronisations with its neighbouring processes. A semi-composition operator takes a process and an interface and restricts the process states and transitions that cannot be reached when considering the traces of the interfaces as the only possible interactions between the process and its environment. In 'Refined Interfaces for Compositional Verification' the author highlights a number of instances where a number of constraints are not captured within these interfaces. During this research talk we shall go through a number of examples that demonstrate this and describe how refined interfaces can be more effective in capturing these constraints. 12th December 2006 Compositional Verification - Part I (Sandro Spina) Abstract: Compositional verification is an instance of enumerative verification which like other verification techniques in this category are confronted with the state explosion problem. This occurs when the number of states to be explored grows exponentially with the number of concurrent processes composed together. With compositional verification we assume that the system being verified can be expressed as a collection of communicating sequential processes. We are then able to replace each sequential process by an abstraction (simpler than the original process) which still preserves the properties to be verified on the whole system. In this research talk we shall investigate the use of interfaces (representing context constraints) to create these process abstractions. 19th December 2006 Compositional Verification - Part II (Sandro Spina) Abstract: Compositional verification is an instance of enumerative verification which like other verification techniques in this category are confronted with the state explosion problem. This occurs when the number of states to be explored grows exponentially with the number of concurrent processes composed together. With compositional verification we assume that the system being verified can be expressed as a collection of communicating sequential processes. We are then able to replace each sequential process by an abstraction (simpler than the original process) which still preserves the properties to be verified on the whole system. In this research talk we shall investigate the use of interfaces (representing context constraints) to create these process abstractions. 12th December 2006 Bisimulation Relations (Sandro Spina) Abstract: A bisimulation is an equivalence relation between labeled transition systems (LTS). During this research talk we will first discuss what a bisimulation is and why we're interested in these relations between LTSs. We then focus on a number of popular bisimulations found in literature including amongst others strong, weak, observational and branching bisimulations. By the end of the hour everyone should be in a position to appreciate the usefulness of these equivalence relations when used for model checking systems.