Add favorite posts
This commit is contained in:
parent
b3dc3e690b
commit
2e3074df00
|
@ -2,6 +2,7 @@
|
||||||
title: "Advent of Code in Coq - Day 1"
|
title: "Advent of Code in Coq - Day 1"
|
||||||
date: 2020-12-02T18:44:56-08:00
|
date: 2020-12-02T18:44:56-08:00
|
||||||
tags: ["Advent of Code", "Coq"]
|
tags: ["Advent of Code", "Coq"]
|
||||||
|
favorite: true
|
||||||
---
|
---
|
||||||
|
|
||||||
The first puzzle of this year's [Advent of Code](https://adventofcode.com) was quite
|
The first puzzle of this year's [Advent of Code](https://adventofcode.com) was quite
|
||||||
|
|
|
@ -3,6 +3,7 @@ title: Compiling a Functional Language Using C++, Part 10 - Polymorphism
|
||||||
date: 2020-03-25T17:14:20-07:00
|
date: 2020-03-25T17:14:20-07:00
|
||||||
tags: ["C and C++", "Functional Languages", "Compilers"]
|
tags: ["C and C++", "Functional Languages", "Compilers"]
|
||||||
description: "In this post, we extend our compiler's typechecking algorithm to implement the Hindley-Milner type system, allowing for polymorphic functions."
|
description: "In this post, we extend our compiler's typechecking algorithm to implement the Hindley-Milner type system, allowing for polymorphic functions."
|
||||||
|
favorite: true
|
||||||
---
|
---
|
||||||
|
|
||||||
[In part 8]({{< relref "08_compiler_llvm.md" >}}), we wrote some pretty interesting programs in our little language.
|
[In part 8]({{< relref "08_compiler_llvm.md" >}}), we wrote some pretty interesting programs in our little language.
|
||||||
|
|
|
@ -2,6 +2,7 @@
|
||||||
title: "How Many Values Does a Boolean Have?"
|
title: "How Many Values Does a Boolean Have?"
|
||||||
date: 2020-08-21T23:05:55-07:00
|
date: 2020-08-21T23:05:55-07:00
|
||||||
tags: ["Java", "Haskell", "C and C++"]
|
tags: ["Java", "Haskell", "C and C++"]
|
||||||
|
favorite: true
|
||||||
---
|
---
|
||||||
|
|
||||||
A friend of mine recently had an interview for a software
|
A friend of mine recently had an interview for a software
|
||||||
|
|
BIN
content/blog/haskell_lazy_evaluation/lazy-fix.zip
Normal file
BIN
content/blog/haskell_lazy_evaluation/lazy-fix.zip
Normal file
Binary file not shown.
BIN
content/blog/haskell_lazy_evaluation/lazy.zip
Normal file
BIN
content/blog/haskell_lazy_evaluation/lazy.zip
Normal file
Binary file not shown.
|
@ -2,6 +2,7 @@
|
||||||
title: Meaningfully Typechecking a Language in Idris, Revisited
|
title: Meaningfully Typechecking a Language in Idris, Revisited
|
||||||
date: 2020-07-22T14:37:35-07:00
|
date: 2020-07-22T14:37:35-07:00
|
||||||
tags: ["Idris"]
|
tags: ["Idris"]
|
||||||
|
favorite: true
|
||||||
---
|
---
|
||||||
|
|
||||||
Some time ago, I wrote a post titled [Meaningfully Typechecking a Language in Idris]({{< relref "typesafe_interpreter.md" >}}). The gist of the post was as follows:
|
Some time ago, I wrote a post titled [Meaningfully Typechecking a Language in Idris]({{< relref "typesafe_interpreter.md" >}}). The gist of the post was as follows:
|
||||||
|
|
Loading…
Reference in New Issue
Block a user