Abstract: Dependent types are a wonderful way to construct correct functional programming and specify interfaces as Edwin has shown in his nice book on type driven development using a welsh dragon. But shall we go further in the esoteric world of homotopy type theory? I will try to motivate this and I am looking forward … Why Homotopy type Theory (HoTT) matters – Professor Thorsten Altenkirch
Abstract: The increasing complexity of codes with the growing number of cores that should be utilised make such codes hard to optimise and maintain. In this talk, we present the OpenMP and MPI refactoring implemented in the ParaFormance tool. This tool transforms the sequential code into parallel code able to run on shared memory machines. … The OpenMP and MPI refactoring with ParaFormance – Turkey Alsalkini
Title: A Type-System for describing System-on-a-Chip Architectures Abstract: The protocols that describe the interactions between IP Cores on System-on-a-Chip (SoC) architectures are well-documented. These protocols described not only the structural properties of the physical interfaces but also the behaviour of the emanating signals. However, there is a disconnect between the design of SoC architectures, their … A Type-System for describing System-on-a-Chip Architectures – Jan De Muijnck-Hughes
Diderot: A Parallel Domain-Specific Language for Image Analysis and Visualization Abstract: The analysis of structure in three-dimensional images is increasingly valuable for biomedical research and computational science. At the same time, the computational burden of processing images is increasing as devices produce images of higher resolution (e.g., typical CT scans have gone from 128^3 to … Diderot: A Parallel Domain-Specific Language for Image Analysis and Visualization – John Reppy
Congratulations to Matus Tejiscak, who successfully defended his thesis yesterday. He is pictured with supervisor Dr Edwin Brady, Internal examiner Dr Chris Jefferson and external examiner Dr Andreas Abel, from the University of Gothenburg.
Abstract: Formal languages and automata are taught to every computer science student. However, the student will most likely not see the beautiful coalgebraic foundations, which use coindutive reasoning. In this talk, I recapitulate how infinite tries can represent formal languages (sets of strings). I explain Agda’s coinduction mechanism based on copatterns and sized types demonstrate … Compositional Coinduction with Sized Types – Dr. Andreas Abel
ARM has a relaxed memory model, previously specified in informal prose for ARMv7 and ARMv8. Over time, and partly due to work building formal semantics for ARM concurrency, it has become clear that some of the complexity of the model is not justified by the potential benefits. In particular, the model was originally non-multicopy-atomic: writes … Simplifying ARM concurrency – Prof. Susmit Sarkar
Title: Efficient Dynamic Mapping of Parallel Applications to NUMA Architectures by Reinforcement Learning Abstract: We present a dynamic framework for mapping threads and data of parallel applications to computational cores/memory nodes of parallel non-uniform memory architecture (NUMA) systems. We use a feedback-based mechanism where the performance of each thread is collected and used to … Dr. Vladimir Janjic – Efficient Dynamic Mapping of Parallel Applications to NUMA Architectures by Reinforcement Learning
Type systems are often presented in a declarative style, but with an emphasis on ensuring that there is some sort of type synthesis algorithm. Since Pierce and Turner’s “Local Type Inference” system, however, there has been a small but growing alternative: bidirectional typing, where types are synthesized for variables and elimination forms, but must always … Bidirectional-Curious? – Dr. Conor McBride