MaisaMilena

def isTeenager: [x]
  if x then: 1 else: 0
  
def isAdult: [x]
  if x then: 1 else: 0

def getCategory: [x]
  if (isTeenager x) 

then: "boring teenager"

MaisaMilena

module Dependently-Typed-Programming-in-Agda where

open import Nat
open import Vector
open import List

{- Studying the book Dependently Typed Programming in Agda by Ulf Norell and James Chapman -}

-- A vector containing n copies of an element x
vec : {n : Nat} {A : Set} -> A -> Vector A n

MaisaMilena

module Parity where

-- Using Human lib
open import Nat
open import Vector
open import List

-- A vector containing n copies of an element x
vec : {n : Nat} {A : Set} -> A -> Vector A n
vec {zero}  x = end

MaisaMilena

The EVM is a stack machine. Instructions might use values on the stack as arguments, and push values onto the stack as results. Let’s consider the operation add.

Elements on the stack are 32-byte words, and all keys and values in storage are 32 bytes. There are over 100 opcodes, divided into categories delineated in multiples of 16.

The EVM is a security oriented virtual machine, designed to permit untrusted code to be executed by a global network of computers.

To do so securely, it imposes the following restrictions:

• Every computational step taken in a program's execution must be paid for up front, thereby preventing Denial-of-Service attacks.
• Programs may only interact with each other by transmitting a single arbitrary-length byte array; they do not have access to each other's state.

MaisaMilena

Agda is a dependently typed functional programming. Dependent type is a type whose definition depends on a value. A "pair of integers" is a type. A "pair of integers where the second is greater than the first" is a dependent type because of the dependence on the value.

• A dependent function's return type may depend on the value (not just type) of an argument. A function that takes a positive integer "n" may return an array of length "n".

• A dependent pair may have a second value that depends on the first. It can be used to encode a pair of integers where the second one is greater than the first.

  A definition is a syntactic construction defining an entity such as a function or a datatype.

  f : (x : A) → B is a dependently typed function, i.e. x can occur in B.

When B does not depend on x we write f : A → B

MaisaMilena

-- 1
-- 10
-- 11
-- 100
-- 101
-- 110
-- 111
-- 1000
-- 1001
-- 1010

MaisaMilena

class Context:
    def __init__(self, list = []):
        self.list = list

    def shift(self, depth, inc):
        new_list = []
        for binder in self.list:
            if binder is None:
                new_list.append(None)
            else: