All student talks will now take place in C60. Format is (up to) 10 minutes for talk, and 5 for questions. Running order (times are approximate):
Just like any other branch of mathematics, denotational semantics of programming languages should be formalised in type theory, but adapting traditional domain theoretic semantics, as originally formulated in classical set theory to type theory has proven challenging. This paper is part of a project on formulating denotational semantics in type theories with guarded recursion. This should have the benefit of not only giving simpler semantics and proofs of properties such as adequacy, but also hopefully in the future to scale to languages with advanced features, such as general references, outside the reach of traditional domain theoretic techniques.
Working in Guarded Dependent Type Theory (GDTT), we develop denotational semantics for FPC, the simply typed lambda calculus extended with recursive types, modelling the recursive types of FPC using the guarded recursive types of GDTT. We prove soundness and computational adequacy of the model in GDTT using a logical relation between syntax and semantics constructed also using guarded recursive types. The denotational semantics is intensional in the sense that it counts the number of unfold-fold reductions needed to compute the value of a term, but we construct a relation relating the denotations of extensionally equal terms, i.e., pairs of terms that compute the same value in a different number of steps. Finally we show how the denotational semantics of terms can be executed inside type theory and prove that executing the denotation of a boolean term computes the same value as the operational semantics of FPC.
We adapt the technique of type-generic programming via descriptions pointing into a universe, to the domain of typed languages with binders and variables, implementing a notion of *syntax-generic programming* in a dependently typed programming language.
We present an Agda library implementation of type-preserving renaming and substitution (including proofs about their behaviour) “once and for all” over all applicable languages using our technique.
This talk discusses a newly started research project expand on Digital Musical Instrument (DMI) design, improving accessibility by targeting low cost microcontrollers. By exploring programming paradigms and tools currently used in the development of both audio hardware and audio applications, this work will formalise a modular framework for the design and implementation of digital musical instruments. The framework will incorporate research on functional languages and domain specific languages to apply the concept of composition to the different domains that make up a DMI, for example the audio domain and control domain. Further, the research will then analyse whether this allows for effective optimisation for each domain and free creativity in the process of design. The notion of composition will be reflected at the hardware level such that multiple microcontrollers may be targeted to individually handle different domains of computation, in a distributed manner.