willurd

Each of these commands will run an ad hoc http static server in your current (or specified) directory, available at http://localhost:8000. Use this power wisely.

Discussion on reddit.

Python 2.x

$ python -m SimpleHTTPServer 8000

sigrlami

WARNING This list outdated, for the up to date version visit https://haskellcosm.com

List of companies that use Haskell in Production

Types of work:

• RD - research&development
• PR - product
• IP - in-house product
• CO - consulting

seankross

AndyShiue

I think I’ve figured out most parts of the cubical type theory papers; I’m going to take a shot to explain it informally in the format of Q&As. I prefer using syntax or terminologies that fit better rather than the more standard ones.

Q: What is cubical type theory?

A: It’s a type theory giving homotopy type theory its computational meaning.

Q: What is homotopy type theory then?

A: It’s traditional type theory (which refers to Martin-Löf type theory in this Q&A) augmented with higher inductive types and the univalence axiom.

kalloc

Latency Comparison Numbers (~2012)
----------------------------------
L1 cache reference                           0.5 ns
Branch mispredict                            5   ns
L2 cache reference                           7   ns                      14x L1 cache
Mutex lock/unlock                           25   ns
Main memory reference                      100   ns                      20x L2 cache, 200x L1 cache
Compress 1K bytes with Zippy             3,000   ns        3 us
Send 1K bytes over 1 Gbps network       10,000   ns       10 us
Read 4K randomly from SSD*             150,000   ns      150 us          ~1GB/sec SSD

MattPD

Program Analysis Resources

(draft; work in progress)

See also:

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

pedrominicz

The originality of these Gists varies drastically. Most are inspired by the work of others, in that case, all merit goes to the original authors. I have linked everything used as reference material on the Gists themselves.

Haskell

• Crégut's strongly reducing Krivine abstract machine
• Type-check STLC into a GADT
• Alex: indentation-sensitive lexer
• A-normalization (administrative normal form, ANF)
• Number of SK-combinator calculus terms of a given size
• Number of untyped lambda calculus terms of a given size

raysan5

CUSTOM GAME ENGINES: A Small Study

A couple of weeks ago I played (and finished) A Plague Tale, a game by Asobo Studio. I was really captivated by the game, not only by the beautiful graphics but also by the story and the locations in the game. I decided to investigate a bit about the game tech and I was surprised to see it was developed with a custom engine by a relatively small studio. I know there are some companies using custom engines but it's very difficult to find a detailed market study with that kind of information curated and updated. So this article.

Nowadays lots of companies choose engines like Unreal or Unity for their games (or that's what lot of people think) because d

martinchapman

# Visualise a latex document git history

# loop through commits, create a PDF from your main file for each
# translate the pages of that PDF to a single image
# create GIF/mp4 from the folder of images created

# run within your local repository
# prerequisites: ImageMagick and FFmpeg

# create output folder

suhr

Упражнения по формальным доказательствам

Нет времени объяснять, переходим сразу к делу.

Инструменты

Доказывать теоремы мы будем, используя интерактивные пруверы Isabelle или Lean 3. Примеры приводятся для каждого прувера, для решения задач же можно использовать любой из них.