Next meeting on Wednesday March 22nd

[Tim McGilchrist]

We have two fantastic talks for March. Tim Hunter is going to give his first presentation at FP-SYD on "Formal language theory from a functional programming perspective", and returning speaker Amos Robinson is going to tell us about Synchronous languages and F*.

Doors open at 6p with talks kicking off around 6:45pm. Please RSVP on meetup or contact the organisers directly, so we can let our hosts know how many to cater for. Abstracts included below.

Cheers,

Tim McGilchrist

-------------------------------

Formal language theory from a functional programming perspective - Tim Hunter

When computer scientists learn about formal language theory or the Chomsky Hierarchy, for example in a course on compilers, it's often mentioned in passing that this theory was first developed for the study of natural human languages. For applications to things like programming languages, some of the very first kinds of grammars to be formulated (e.g. finite-state grammars, context-free grammars) turned out to be more or less sufficient. But applications to the study of natural languages have prompted the development of many more kinds of formal grammars, and the details of these more recent developments can often be usefully understood through the lens of ideas that are central to functional programming, such as folds on recursive data structures.

In this talk I'll give a brief overview of the role formal language theory plays in the study of natural languages, and use functional programming concepts as a framework to introduce some of the more recent kinds of grammars that have been developed for specifically linguistic purposes.

-------------------------------
Closed-form semantics for a synchronous language, mechanised in F* - Amos Robinson

Synchronous languages like Lustre are used for safety-critical applications, such as the control system for a nuclear reactor. Unfortunately, these languages usually have their semantics defined relationally, rather than as a "closed form" that can be directly computed, and I've always found them a bit confusing. Having a closed-form solution is a useful property, as programs can be evaluated by directly applying the rules of the semantics.

In this talk, I will introduce a closed-form semantics for a small unclocked Lustre-style language. Although this new semantics has the wrong complexity (!), the evaluation rules are simple and I think that it will be easier to understand and reason about than the relational semantics. I will also describe my experience using F* to formalise this language.