Recently, I’ve been reading a series of papers by Lauren Bramblett, Nicola Bezzo, and their collaborators, on improving multirobot systems using epistemic reasoning - that is, reasoning about other robots’ knowledge and beliefs. This line of work is quite far from my research area; however, given the papers’ references to epistemic logic and my interest in logic in general and background in embedded systems, it appeared to be an interesting read. I was not disappointed, quite the contrary - the papers surprised me.

Read more...

One thing I like on theorem proving is that committing to providing a proof of key properties of some artifact, be it a software program or a mathematical definition, creates a pressure to structure the artifact in a way that is amenable to precise reasoning. Hence, artifacts which are equipped with proofs of key properties, are, in my experience, easier to understand then those which are not equipped with such proofs. So, when practicing theorem proving, I am generally happy about the resulting definitions or programs. However, I am not that happy about the structure of the proofs that I produce.

Read more...

A few days ago I watched a recording of Michael Wooldridge’s talk titled “This is not the AI we were promised”. The talk was informative and really fun to watch. However, what caught my attention the most was not the technical content of the talk, but the communicational/pedagogical approach prof. Wooldridge took. Consequently, it made me reflect on my own style of communication and on ways to improve it.

Read more...

Embedded Linux is everywhere. When it comes to building bootable images of Linux-based operating system, there exist popular toolchains such as Yocto and Buildroot. In this post I explore an alternative approach, using a tool known as Nix. The approach is mechanically reproducible and keeps me in the control.

Read more...

Robustness and correctness are certainly desirable properties of a piece of software. So is performance. Certain mainstream approaches to robustness, such as dynamic checks, have negative performance effects, which may create the impression that robustness or correstness is fundamentally at odds with performance. But is it really the case?

Read more...

In Minuska, one can describe the semantics of a programming language using term rewriting. As term rewriting is quite low-level and expressing common patterns is repetitive, Minuska, inspired by the K-framework, implements some shortcuts (“syntactic sugar”) whose meaning is defined only by their translation to term rewriting rules. This post motivates the need for and presents a design of a higher-level language-description language that I plan to implement into Minuska.

Read more...

I am weighting my options on future research directions.

Read more...

Here a present an idea for a simple tool for information flow control. As usually, the idea is language-parametric.

Read more...

There is one aspect of the Minuska framework which provides a language designer a great flexibility. Namely, a programming language configuration is a tree whose leaves hold values from an arbitrary domain (typically integers, lists, etc); it is up to the language designer to choose a suitable domain. This makes writing language-parametric tools in Minuska even harder. In this post I explore some arguments for supporting domain-parametricity anyway, discuss the associated problems, and sketch out a possible solution.

Read more...

In order to be useful, data stored in computer need to represent real-world phenomena. However, making the representation go through an extra level of indirection – through the realm of mathematics – can be benefitial.

Read more...