brendanzab

Inference Rules

Natural deduction

T ::=
  | Int
  | Bool

t1, t2 ::=

brendanzab

Quantifiers

Idea: create a surface syntax where all quantifiers behave more like records/modules with labelled entries.

Examples

{
 out id : {

brendanzab

Notation	Meaning
l ? T	abstract node in T
l : T	concrete node in T
l = t	node equal to t
default = t	reduce to this node if all nodes are concrete
{ ... }	graph term
t1.{ l = t2 }	updates node l in t1 to be t2
t.l	gets the value of node l in t
t.{ l1 -> l2 }	renames l1 to l2 in t

brendanzab

Combining Pi and Sigma types?

-- id : forall a. a -> a
-- id x = x

id : type [
    in A : Type, 
    in a : A, 
    out a' : A,

brendanzab

A graph-based core for a dependently typed language

Abstract

An overly-ambitious attempt to re-think the core calculus of dependent type theory by basing it on graphs as opposed to lambdas, Π-types, Σ-types, etc. The hope is that this might allow us to investigate dependency more closely, and allow us to refine programs to target different environments in an easier way than with traditional programming representations.

Introduction

brendanzab

{
  "record.term": {
    "fields": {
      "identity": { "node": "$identity" },
      "compose": { "node": "$compose" },
      "Unit": { "node": "$Unit" },
      "Bool": { "node": "$Bool" },
      "Option": { "node": "$Option" }
    },
    "nodes": {

brendanzab

# Concrete syntax:
#
# ```
# let
#   pi
#     : float/64
#     = 3.1415
#   identity ||< The polymorphic identity function
#     : [ A : Type  ||< The input type.
#       , a : A     ||< The input.

pvieito

Twitter API Keys

Twitter for iPhone

Consumer key: IQKbtAYlXLripLGPWd0HUA
Consumer secret: GgDYlkSvaPxGxC4X8liwpUoqKwwr3lCADbz8A7ADU

Twitter for Android

Consumer key: 3nVuSoBZnx6U4vzUxf5w
Consumer secret: Bcs59EFbbsdF6Sl9Ng71smgStWEGwXXKSjYvPVt7qys

Twitter for Google TV

Consumer key: iAtYJ4HpUVfIUoNnif1DA

briansmith

How to Generate & Use Private Keys using OpenSSL's Command Line Tool

These commands generate and use private keys in unencrypted binary (not Base64 “PEM”) PKCS#8 format. The PKCS#8 format is used here because it is the most interoperable format when dealing with software that isn't based on OpenSSL.

OpenSSL has a variety of commands that can be used to operate on private key files, some of which are specific to RSA (e.g. openssl rsa and openssl genrsa) or which have other limitations. Here we always use

seanjensengrey

This is a small demo of how to create a library in Rust and call it from Python (both CPython and PyPy) using the CFFI instead of ctypes.

Based on http://harkablog.com/calling-rust-from-c-and-python.html (dead) which used ctypes

CFFI is nice because:

• Reads C declarations (parses headers)
• Works in both CPython and PyPy (included with PyPy)
• Lower call overhead than ctypes