This post is based on the paper by Thomas Austin and Cormac Flanagan. A value can be read by some entity who has the proper authority to read it. A value <k ? s : p> means an entity with authority label k or higher will see the value s, otherwise it will see p. They have evaluation semantics for faceted values. And they also have a concept of view. L: Faceted_Value → value Equivalnce of view, if V1 eqv V2 then L(V1) = L(V2)

Compilers convert source language to target language. Sometimes they take one pass, and sometimes they take multiple passes. We need to make sure the compiled language in each pass retains all the security properties of the source language : The goal of secure compilation techniques is to ensure this particular…

This paper is written by Rodrigous and Liskov. There are two important liveness aspects in BFT. Fault detection and recovery. With remote attestation, i.e. secure hardware, fault detection is easy but recovery is not possible. With proactive recovery detecting faults is not possible but recovery from certain attacks is possible. Proactive recovery is when each node is monitored by a watch-dog periodically and restarted with reinitialised code upon some failure.

6: Laziness Suggested reading: In the first lesson, I mentioned that Haskell is lazy, and promised to eventually explain in more…www.schoolofhaskell.com Side effects and purity So, what’s really at issue here is the presence or absence of side effects. By “side effect” we mean anything that causes evaluation of an expression to interact with something outside itself. The root issue is that such outside interactions are time-sensitive. For example:

let x = z^2 in if cond then x+y else 1 In the above code x is used only in then branch and not it else branch, and which branch is chosen depends on cond. So, it is totally unnecessary and waste of resources to evaluate x beforehand. It is…

A higher order function is a function that can take a function as a parameter and/or can return a function as its end result. In this post we will discuss a few popular Haskell higher order functions. Filter As the name suggests this function filters out data that satisfy some condition. …

When we write that a function F has type a → b → c, we can say two things about it. the function takes two parameters of type a and b and returns a type c. [i.e. (a → b) → c ] Or, the function takes a parameter of…

Let us talk about the most popular typeclass in Haskell, i.e. monads. The main usage of monads in Haskell is to make effects wrap inside a context, so that it has a type. …

First, let us see what algebraic structures are. An algebraic structure comprises of three parts: a set of elements, a set of operations on the elements with finite arity, and a set of identity elements. Monoid is an algebraic structure with an associative binary operation and an identity element. …