Circular Image

D. Spinellis

14 records found

Productively recursing infinitely

Modelling evaluation of lambda calculus with coinduction in Agda

Coinduction is used to model infinite data or cycles in Agda. However, it is not as well explored in Agda as induction. Therefore, support for it might be lacking compared to induction. I explore how this applies for the evaluation of lambda calculus, what the different encodings ...

Modelling cyclic structures in Agda

Coinductive formalizations of Linear Temporal Logic

This thesis explores the formalization of Linear Temporal Logic (LTL) within the Agda proof assistant, focusing on the use of coinductive techniques to model infinite structures. Two primary questions guide this investigation: how can coinduction be employed to represent LTL form ...

Encoding Finite State Automata in Agda using coinduction

Evaluating the support for coinduction in Agda

The proof assistant Agda supports coinduction, which can be used to reason about infinite and cyclic structures. The possibilities and limitations of using coinduction in Agda are not well known. To better understand these, I will implement Finite State Automata and their equival ...

Stuck in a (While) Loop

Assessing Coinduction in Agda using Cyclic Program Traces

Interactive proof assistants such as Agda have powerful applications in proving the correctness of software. Non-terminating programs, such as those containing infinite loops, result in execution paths of infinite length, which can introduce challenges when reasoning about such p ...

Modelling cyclic structures in Agda

Evaluating Agda's coinduction through modelling graphs

Graphs are a widely used concept within computer science. Modelling graphs can be done in various ways, but the most popular approach is doing so inductively. When graphs contain cycles modelling them becomes less intuitive. A solution for this is using the dual of induction call ...
Interpreted applications are often vulnerable to remote code execution attacks. To protect interpreted applications, we should reduce the tools available to the attackers. In this thesis, we investigate the possibilities for the automation of policy generation for interpreted app ...
As the world continues to embrace cloud computing, more applications are being scaled elastically. Elastic scaling allows applications to add or remove computing resources based on the load experienced by the application. When the load is high more resources are provisioned enabl ...
Anonymity networks, such as The Invisible Internet Project, commonly known as I2P, enable privacy aware users to stay anonymous on the Internet and provide secure methods of communication, as well as multi-layered encryption. Despite the many innocent reasons users opt for online ...
Users of anonymity networks face differential treatment and sometimes get blocked by websites, it is currently unclear how common this blocking is. This research aims to provide an overview of how common this blocking is while utilizing the AN.ON anonymity network. The analysis i ...
Censorship and privacy issues have led people to use VPNs when accessing the internet. These VPNs not only try to protect their user but they are also associated with criminality and cyber attacks. Because of this, websites have started to resort to blacklisting the IP addresses ...
The Bitcoin Lightning Network is a layer-two solution that promises instant payments, scalability, and low transaction fees on top of the Bitcoin blockchain. In case there is no direct channel between the sender and receiver, the routing algorithm uses source routing and a shorte ...
The LND is currently the most popular routing algorithm used in the Lightning Network, the second layer solution to Bitcoin’s scalability. Despite its popularity, recent studies demonstrate that its deterministic nature compromises the anonymity of the Lightning Network. In other ...
The Lightning Network is a second layer payment protocol built on top of Bitcoin, which is scalable and has reduced transaction fees. It does so by eliminating the need to broadcast every transaction to the whole network. When one user wants to send a payment to another, the rout ...
Tor is the most popular tool for anonymous online communication. However, the performance of Tor's volunteer-run network is suboptimal when network congestion occurs. Within Tor, many connections are multiplexed over a single TCP connection between relays, which causes a head-of- ...