arXiv subjects

Boro Sitnikovski

Publications and source records attributed to Boro Sitnikovski.

4 recordsLinked to original sources

arXiv2022

Budge: a programming language and a theorem prover

We present a simple programming language based on Gödel numbering and prime factorization, enhanced with explicit, scoped loops, allowing for easy program composition. Further, we will present a theorem prover that allows expressing and working with formal systems. The theorem prover is simple as it relies merely on a substitution rule and set equality to derive theorems. Finally, we will represent the programming language in the theorem prover. We will show the syntax and semantics of both, and then provide a few example programs and their evaluation.

cs.PL↗

arXiv2021

Tutorial implementation of Hoare logic in Haskell

Using the programming language Haskell, we introduce an implementation of propositional calculus, number theory, and a simple imperative language that can evaluate arithmetic and boolean expressions. Finally, we provide an implementation of Hoare's logic which will allow us to deduce facts about programs without the need for a full evaluation.

cs.PL↗

arXiv2020

Formalizing line editors in Coq

Text editors represent one of the fundamental tools that writers use - software developers, book authors, mathematicians. A text editor must work as intended in that it should allow the users to do their job. We start by introducing a small subset of a text editor - line editor. Next, we will give a concrete definition (specification) of what a complete text editor means. Afterward, we will provide an implementation of a line editor in Coq, and then we will prove that it is a complete text editor.

cs.LO↗

arXiv2020

PubSub implementation in Haskell with formal verification in Coq

In the cloud, the technology is used on-demand without the need to install anything on the desktop. Software as a Service is one of the many cloud architectures. The PubSub messaging pattern is a cloud-based Software as a Service solution used in complex systems, especially in the notifications part where there is a need to send a message from one unit to another single unit or multiple units. Haskell is a generic typed programming language which has pioneered several advanced programming language features. Based on the lambda calculus system, it belongs to the family of functional programming languages. Coq, also based on a stricter version of lambda calculus, is a programming language that has a more advanced type system than Haskell and is mainly used for theorem proving i.e. proving software correctness. This paper aims to show how PubSub can be used in conjunction with cloud computing (Software as a Service), as well as to present an example implementation in Haskell and proof of correctness in Coq.

cs.PL↗