ndmitchell

{-# LANGUAGE StaticPointers #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE FlexibleInstances #-}

import Data.Binary
import System.IO.Unsafe
import GHC.StaticPtr

shagunsodhani

Deep Math: Deep Sequence Models for Premise Selection

Introduction

• Automated Theorem Proving (ATP) - Attempting to prove mathematical theorems automatically.
• Bottlenecks in ATP:
  • Autoformalization - Semantic or formal parsing of informal proofs.
  • Automated Reasoning - Reasoning about already formalised proofs.
• Paper evaluates the effectiveness of neural sequence models for premise selection (related to automated reasoning) without using hand engineered features.
• Link to the paper

jc00ke

#!/usr/bin/env sh

sudo update-alternatives --install \
        /usr/bin/llvm-config       llvm-config      /usr/bin/llvm-config-3.4  200 \
--slave /usr/bin/llvm-ar           llvm-ar          /usr/bin/llvm-ar-3.4 \
--slave /usr/bin/llvm-as           llvm-as          /usr/bin/llvm-as-3.4 \
--slave /usr/bin/llvm-bcanalyzer   llvm-bcanalyzer  /usr/bin/llvm-bcanalyzer-3.4 \
--slave /usr/bin/llvm-cov          llvm-cov         /usr/bin/llvm-cov-3.4 \
--slave /usr/bin/llvm-diff         llvm-diff        /usr/bin/llvm-diff-3.4 \
--slave /usr/bin/llvm-dis          llvm-dis         /usr/bin/llvm-dis-3.4 \

albanpeignier

/* 
  A Minimal Capture Program

  This program opens an audio interface for capture, configures it for
  stereo, 16 bit, 44.1kHz, interleaved conventional read/write
  access. Then its reads a chunk of random data from it, and exits. It
  isn't meant to be a real program.

  From on Paul David's tutorial : http://equalarea.com/paul/alsa-audio.html