larrytheliquid

open import Data.Empty using ( ⊥ ; ⊥-elim )
open import Data.Unit using ( ⊤ ; tt )
open import Data.Bool using ( Bool ; true ; false ; if_then_else_ )
  renaming ( _≟_ to _≟B_ )
open import Data.Nat using ( ℕ ; zero ; suc )
    renaming ( _≟_ to _≟ℕ_ )
open import Data.Product using ( Σ ; _,_ )
open import Relation.Nullary using ( Dec ; yes ; no )
open import Relation.Binary using ( Decidable )
open import Relation.Binary.PropositionalEquality using ( _≡_ ; refl )

chrisdone

Typing Haskell in Haskell

MARK P. JONES

Pacific Software Research Center

Department of Computer Science and Engineering

Oregon Graduate Institute of Science and Technology

fairlight1337

// This code installs a custom signal handler for the SIGSEGV signal
// (segmentation fault) and then purposefully creates a segmentation
// fault. The custom handler `handler` is then entered, which now
// increases the instruction pointer by 1, skipping the current byte
// of the faulty instruction. This is done for as long as the faulty
// instruction is still active; in the below case, that's 2 bytes.

// Note: This is for 64 bit systems. If you prefer 32 bit, change
// `REG_RIP` to `REG_EIP`. I didn't bother putting an appropriate
// `#ifdef` here.

MattPD

Program Analysis Resources

(draft; work in progress)

See also:

• Compilers
  • correctness
• Program analysis:
• Dynamic analysis - instrumentation, translation, sanitizers

bobatkey

{-# OPTIONS --rewriting #-}

module cont-cwf where

open import Agda.Builtin.Sigma
open import Agda.Builtin.Unit
open import Agda.Builtin.Bool
open import Agda.Builtin.Nat
open import Data.Empty
import Relation.Binary.PropositionalEquality as Eq

vivshaw

If you want to see how it works, see the README on the repo.

pervognsen

// Estimating CPU frequency...
// CPU frequency: 4.52 GHz
// sum1: value = 15182118497126522709, 0.31 secs, 5.14 cycles/elem
// sum2: value = 15182118497126522709, 0.17 secs, 2.93 cycles/elem

#define RW(x) asm("" : "+r"(x))

typedef struct Node {
	u64 value;
	struct Node *next;

isti115

{-# OPTIONS --rewriting #-}
module sknorm where

open import Agda.Primitive
open import Level
open import Relation.Binary.PropositionalEquality
open import Agda.Builtin.Equality.Rewrite
open import Data.Product
open import Data.Empty

RealNeGate

// Compile with clang or MSVC (WINDOWS ONLY RN)
//
// Implementing a POC green threads system using safepoints to show how cheap and simple it can
// be done, all you need to do is call SAFEPOINT_POLL in your own language at the top of every
// loop and function body (you can loosen up on this depending on the latency of pausing you're
// willing to pay). Safepoint polling is made cheap because it's a load without a use site
// which means it doesn't introduce a stall and pays a sub-cycle cost because of it (wastes resources
// sure but doesn't block up the rest of execution).
//
//  # safepoint poll

wilbowma

{-# OPTIONS --guarded #-}


open import Agda.Primitive
open import Relation.Binary.PropositionalEquality using (_≡_; refl; subst; sym; trans)
open import Data.Unit using (⊤; tt)
open import Data.Nat -- using (ℕ; _+_; suc; _<_)
open import Data.Nat.Properties
open import Data.Fin using (Fin; fromℕ; fromℕ<)
open import Data.Vec using (Vec; lookup; []; _∷_; [_]; _++_; map)