Compare commits
4 Commits
846d85bb7a
...
5384faf3ec
Author | SHA1 | Date | |
---|---|---|---|
5384faf3ec | |||
a833cd84f3 | |||
7f1b9d31ea | |||
5bd8c11a86 |
|
@ -6,6 +6,12 @@ summaryLength = 20
|
||||||
|
|
||||||
defaultContentLanguage = 'en'
|
defaultContentLanguage = 'en'
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
[taxonomies]
|
||||||
|
tag = 'tags'
|
||||||
|
series = "series"
|
||||||
|
|
||||||
[outputFormats]
|
[outputFormats]
|
||||||
[outputFormats.Toml]
|
[outputFormats.Toml]
|
||||||
name = "toml"
|
name = "toml"
|
||||||
|
|
|
@ -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"]
|
||||||
|
series: "Advent of Code in Coq"
|
||||||
favorite: true
|
favorite: true
|
||||||
---
|
---
|
||||||
|
|
||||||
|
|
|
@ -2,6 +2,7 @@
|
||||||
title: Compiling a Functional Language Using C++, Part 0 - Intro
|
title: Compiling a Functional Language Using C++, Part 0 - Intro
|
||||||
date: 2019-08-03T01:02:30-07:00
|
date: 2019-08-03T01:02:30-07:00
|
||||||
tags: ["C and C++", "Functional Languages", "Compilers"]
|
tags: ["C and C++", "Functional Languages", "Compilers"]
|
||||||
|
series: "Compiling a Functional Language using C++"
|
||||||
description: "In this first post of a larger series, we embark on a journey of developing a compiler for a lazily evaluated functional language."
|
description: "In this first post of a larger series, we embark on a journey of developing a compiler for a lazily evaluated functional language."
|
||||||
---
|
---
|
||||||
During my last academic term, I was enrolled in a compilers course.
|
During my last academic term, I was enrolled in a compilers course.
|
||||||
|
|
|
@ -2,6 +2,7 @@
|
||||||
title: A Language for an Assignment - Homework 1
|
title: A Language for an Assignment - Homework 1
|
||||||
date: 2019-12-27T23:27:09-08:00
|
date: 2019-12-27T23:27:09-08:00
|
||||||
tags: ["Haskell", "Python", "Algorithms", "Programming Languages"]
|
tags: ["Haskell", "Python", "Algorithms", "Programming Languages"]
|
||||||
|
series: "A Language for an Assignment"
|
||||||
---
|
---
|
||||||
|
|
||||||
On a rainy Oregon day, I was walking between classes with a group of friends.
|
On a rainy Oregon day, I was walking between classes with a group of friends.
|
||||||
|
|
|
@ -2,6 +2,7 @@
|
||||||
title: "Everything I Know About Types: Introduction"
|
title: "Everything I Know About Types: Introduction"
|
||||||
date: 2022-06-26T18:36:01-07:00
|
date: 2022-06-26T18:36:01-07:00
|
||||||
tags: ["Type Systems", "Programming Languages"]
|
tags: ["Type Systems", "Programming Languages"]
|
||||||
|
series: "Everything I Know About Types"
|
||||||
draft: true
|
draft: true
|
||||||
---
|
---
|
||||||
|
|
||||||
|
|
|
@ -2,6 +2,7 @@
|
||||||
title: "Advent of Code in Coq - Day 8"
|
title: "Advent of Code in Coq - Day 8"
|
||||||
date: 2021-01-10T22:48:39-08:00
|
date: 2021-01-10T22:48:39-08:00
|
||||||
tags: ["Advent of Code", "Coq"]
|
tags: ["Advent of Code", "Coq"]
|
||||||
|
series: "Advent of Code in Coq"
|
||||||
---
|
---
|
||||||
|
|
||||||
Huh? We're on day 8? What happened to days 2 through 7?
|
Huh? We're on day 8? What happened to days 2 through 7?
|
||||||
|
|
|
@ -2,6 +2,7 @@
|
||||||
title: Compiling a Functional Language Using C++, Part 1 - Tokenizing
|
title: Compiling a Functional Language Using C++, Part 1 - Tokenizing
|
||||||
date: 2019-08-03T01:02:30-07:00
|
date: 2019-08-03T01:02:30-07:00
|
||||||
tags: ["C and C++", "Functional Languages", "Compilers"]
|
tags: ["C and C++", "Functional Languages", "Compilers"]
|
||||||
|
series: "Compiling a Functional Language using C++"
|
||||||
description: "In this post, we tackle the first component of our compiler: tokenizing."
|
description: "In this post, we tackle the first component of our compiler: tokenizing."
|
||||||
---
|
---
|
||||||
It makes sense to build a compiler bit by bit, following the stages we outlined in
|
It makes sense to build a compiler bit by bit, following the stages we outlined in
|
||||||
|
|
|
@ -2,6 +2,7 @@
|
||||||
title: A Language for an Assignment - Homework 2
|
title: A Language for an Assignment - Homework 2
|
||||||
date: 2019-12-30T20:05:10-08:00
|
date: 2019-12-30T20:05:10-08:00
|
||||||
tags: ["Haskell", "Python", "Algorithms", "Programming Languages"]
|
tags: ["Haskell", "Python", "Algorithms", "Programming Languages"]
|
||||||
|
series: "A Language for an Assignment"
|
||||||
---
|
---
|
||||||
|
|
||||||
After the madness of the
|
After the madness of the
|
||||||
|
|
|
@ -2,6 +2,7 @@
|
||||||
title: "Everything I Know About Types: Basics"
|
title: "Everything I Know About Types: Basics"
|
||||||
date: 2022-06-30T19:08:50-07:00
|
date: 2022-06-30T19:08:50-07:00
|
||||||
tags: ["Type Systems", "Programming Languages"]
|
tags: ["Type Systems", "Programming Languages"]
|
||||||
|
series: "Everything I Know About Types"
|
||||||
draft: true
|
draft: true
|
||||||
---
|
---
|
||||||
|
|
||||||
|
|
|
@ -2,6 +2,7 @@
|
||||||
title: Compiling a Functional Language Using C++, Part 2 - Parsing
|
title: Compiling a Functional Language Using C++, Part 2 - Parsing
|
||||||
date: 2019-08-03T01:02:30-07:00
|
date: 2019-08-03T01:02:30-07:00
|
||||||
tags: ["C and C++", "Functional Languages", "Compilers"]
|
tags: ["C and C++", "Functional Languages", "Compilers"]
|
||||||
|
series: "Compiling a Functional Language using C++"
|
||||||
description: "In this post, we combine our compiler's tokenizer with a parser, allowing us to extract structure from input source code."
|
description: "In this post, we combine our compiler's tokenizer with a parser, allowing us to extract structure from input source code."
|
||||||
---
|
---
|
||||||
In the previous post, we covered tokenizing. We learned how to convert an input string into logical segments, and even wrote up a tokenizer to do it according to the rules of our language. Now, it's time to make sense of the tokens, and parse our language.
|
In the previous post, we covered tokenizing. We learned how to convert an input string into logical segments, and even wrote up a tokenizer to do it according to the rules of our language. Now, it's time to make sense of the tokens, and parse our language.
|
||||||
|
|
|
@ -2,6 +2,7 @@
|
||||||
title: A Language for an Assignment - Homework 3
|
title: A Language for an Assignment - Homework 3
|
||||||
date: 2020-01-02T22:17:43-08:00
|
date: 2020-01-02T22:17:43-08:00
|
||||||
tags: ["Haskell", "Python", "Algorithms", "Programming Languages"]
|
tags: ["Haskell", "Python", "Algorithms", "Programming Languages"]
|
||||||
|
series: "A Language for an Assignment"
|
||||||
---
|
---
|
||||||
|
|
||||||
It rained in Sunriver on New Year's Eve, and it continued to rain
|
It rained in Sunriver on New Year's Eve, and it continued to rain
|
||||||
|
|
|
@ -2,6 +2,7 @@
|
||||||
title: "Everything I Know About Types: Variables"
|
title: "Everything I Know About Types: Variables"
|
||||||
date: 2022-08-28T19:05:31-07:00
|
date: 2022-08-28T19:05:31-07:00
|
||||||
tags: ["Type Systems", "Programming Languages"]
|
tags: ["Type Systems", "Programming Languages"]
|
||||||
|
series: "Everything I Know About Types"
|
||||||
draft: true
|
draft: true
|
||||||
---
|
---
|
||||||
|
|
||||||
|
|
|
@ -2,6 +2,7 @@
|
||||||
title: Compiling a Functional Language Using C++, Part 3 - Type Checking
|
title: Compiling a Functional Language Using C++, Part 3 - Type Checking
|
||||||
date: 2019-08-06T14:26:38-07:00
|
date: 2019-08-06T14:26:38-07:00
|
||||||
tags: ["C and C++", "Functional Languages", "Compilers"]
|
tags: ["C and C++", "Functional Languages", "Compilers"]
|
||||||
|
series: "Compiling a Functional Language using C++"
|
||||||
description: "In this post, we allow our compiler to throw away invalid programs, detected using a monomorphic typechecking algorithm."
|
description: "In this post, we allow our compiler to throw away invalid programs, detected using a monomorphic typechecking algorithm."
|
||||||
---
|
---
|
||||||
I think tokenizing and parsing are boring. The thing is, looking at syntax
|
I think tokenizing and parsing are boring. The thing is, looking at syntax
|
||||||
|
|
|
@ -2,6 +2,7 @@
|
||||||
title: Compiling a Functional Language Using C++, Part 4 - Small Improvements
|
title: Compiling a Functional Language Using C++, Part 4 - Small Improvements
|
||||||
date: 2019-08-06T14:26:38-07:00
|
date: 2019-08-06T14:26:38-07:00
|
||||||
tags: ["C and C++", "Functional Languages", "Compilers"]
|
tags: ["C and C++", "Functional Languages", "Compilers"]
|
||||||
|
series: "Compiling a Functional Language using C++"
|
||||||
description: "In this post, we take a little break from pushing our compiler forward to make some improvements to the code we've written so far."
|
description: "In this post, we take a little break from pushing our compiler forward to make some improvements to the code we've written so far."
|
||||||
---
|
---
|
||||||
We've done quite a big push in the previous post. We defined
|
We've done quite a big push in the previous post. We defined
|
||||||
|
|
|
@ -2,6 +2,7 @@
|
||||||
title: Compiling a Functional Language Using C++, Part 5 - Execution
|
title: Compiling a Functional Language Using C++, Part 5 - Execution
|
||||||
date: 2019-08-06T14:26:38-07:00
|
date: 2019-08-06T14:26:38-07:00
|
||||||
tags: ["C and C++", "Functional Languages", "Compilers"]
|
tags: ["C and C++", "Functional Languages", "Compilers"]
|
||||||
|
series: "Compiling a Functional Language using C++"
|
||||||
description: "In this post, we define the rules for a G-machine, the abstract machine that we will target with our compiler."
|
description: "In this post, we define the rules for a G-machine, the abstract machine that we will target with our compiler."
|
||||||
---
|
---
|
||||||
{{< gmachine_css >}}
|
{{< gmachine_css >}}
|
||||||
|
|
|
@ -2,6 +2,7 @@
|
||||||
title: Compiling a Functional Language Using C++, Part 6 - Compilation
|
title: Compiling a Functional Language Using C++, Part 6 - Compilation
|
||||||
date: 2019-08-06T14:26:38-07:00
|
date: 2019-08-06T14:26:38-07:00
|
||||||
tags: ["C and C++", "Functional Languages", "Compilers"]
|
tags: ["C and C++", "Functional Languages", "Compilers"]
|
||||||
|
series: "Compiling a Functional Language using C++"
|
||||||
description: "In this post, we enable our compiler to convert programs written in our functional language to G-machine instructions."
|
description: "In this post, we enable our compiler to convert programs written in our functional language to G-machine instructions."
|
||||||
---
|
---
|
||||||
In the previous post, we defined a machine for graph reduction,
|
In the previous post, we defined a machine for graph reduction,
|
||||||
|
|
|
@ -2,6 +2,7 @@
|
||||||
title: Compiling a Functional Language Using C++, Part 7 - Runtime
|
title: Compiling a Functional Language Using C++, Part 7 - Runtime
|
||||||
date: 2019-08-06T14:26:38-07:00
|
date: 2019-08-06T14:26:38-07:00
|
||||||
tags: ["C and C++", "Functional Languages", "Compilers"]
|
tags: ["C and C++", "Functional Languages", "Compilers"]
|
||||||
|
series: "Compiling a Functional Language using C++"
|
||||||
description: "In this post, we implement the supporting code that will be shared between all executables our compiler will create."
|
description: "In this post, we implement the supporting code that will be shared between all executables our compiler will create."
|
||||||
---
|
---
|
||||||
Wikipedia has the following definition for a __runtime__:
|
Wikipedia has the following definition for a __runtime__:
|
||||||
|
|
|
@ -2,6 +2,7 @@
|
||||||
title: Compiling a Functional Language Using C++, Part 8 - LLVM
|
title: Compiling a Functional Language Using C++, Part 8 - LLVM
|
||||||
date: 2019-10-30T22:16:22-07:00
|
date: 2019-10-30T22:16:22-07:00
|
||||||
tags: ["C and C++", "Functional Languages", "Compilers"]
|
tags: ["C and C++", "Functional Languages", "Compilers"]
|
||||||
|
series: "Compiling a Functional Language using C++"
|
||||||
description: "In this post, we enable our compiler to convert G-machine instructions to LLVM IR, which finally allows us to generate working executables."
|
description: "In this post, we enable our compiler to convert G-machine instructions to LLVM IR, which finally allows us to generate working executables."
|
||||||
---
|
---
|
||||||
|
|
||||||
|
|
|
@ -2,6 +2,7 @@
|
||||||
title: Compiling a Functional Language Using C++, Part 9 - Garbage Collection
|
title: Compiling a Functional Language Using C++, Part 9 - Garbage Collection
|
||||||
date: 2020-02-10T19:22:41-08:00
|
date: 2020-02-10T19:22:41-08:00
|
||||||
tags: ["C and C++", "Functional Languages", "Compilers"]
|
tags: ["C and C++", "Functional Languages", "Compilers"]
|
||||||
|
series: "Compiling a Functional Language using C++"
|
||||||
description: "In this post, we implement a garbage collector that frees memory no longer used by the executables our compiler creates."
|
description: "In this post, we implement a garbage collector that frees memory no longer used by the executables our compiler creates."
|
||||||
---
|
---
|
||||||
|
|
||||||
|
|
|
@ -2,6 +2,7 @@
|
||||||
title: Compiling a Functional Language Using C++, Part 10 - Polymorphism
|
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"]
|
||||||
|
series: "Compiling a Functional Language using C++"
|
||||||
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
|
favorite: true
|
||||||
---
|
---
|
||||||
|
|
|
@ -2,6 +2,7 @@
|
||||||
title: Compiling a Functional Language Using C++, Part 11 - Polymorphic Data Types
|
title: Compiling a Functional Language Using C++, Part 11 - Polymorphic Data Types
|
||||||
date: 2020-04-14T19:05:42-07:00
|
date: 2020-04-14T19:05:42-07:00
|
||||||
tags: ["C and C++", "Functional Languages", "Compilers"]
|
tags: ["C and C++", "Functional Languages", "Compilers"]
|
||||||
|
series: "Compiling a Functional Language using C++"
|
||||||
description: "In this post, we enable our compiler to understand polymorphic data types."
|
description: "In this post, we enable our compiler to understand polymorphic data types."
|
||||||
---
|
---
|
||||||
[In part 10]({{< relref "10_compiler_polymorphism.md" >}}), we managed to get our
|
[In part 10]({{< relref "10_compiler_polymorphism.md" >}}), we managed to get our
|
||||||
|
|
|
@ -2,6 +2,7 @@
|
||||||
title: Compiling a Functional Language Using C++, Part 12 - Let/In and Lambdas
|
title: Compiling a Functional Language Using C++, Part 12 - Let/In and Lambdas
|
||||||
date: 2020-06-21T00:50:07-07:00
|
date: 2020-06-21T00:50:07-07:00
|
||||||
tags: ["C and C++", "Functional Languages", "Compilers"]
|
tags: ["C and C++", "Functional Languages", "Compilers"]
|
||||||
|
series: "Compiling a Functional Language using C++"
|
||||||
description: "In this post, we extend our language with let/in expressions and lambda functions."
|
description: "In this post, we extend our language with let/in expressions and lambda functions."
|
||||||
---
|
---
|
||||||
|
|
||||||
|
|
|
@ -2,6 +2,7 @@
|
||||||
title: Compiling a Functional Language Using C++, Part 13 - Cleanup
|
title: Compiling a Functional Language Using C++, Part 13 - Cleanup
|
||||||
date: 2020-09-19T16:14:13-07:00
|
date: 2020-09-19T16:14:13-07:00
|
||||||
tags: ["C and C++", "Functional Languages", "Compilers"]
|
tags: ["C and C++", "Functional Languages", "Compilers"]
|
||||||
|
series: "Compiling a Functional Language using C++"
|
||||||
description: "In this post, we clean up our compiler."
|
description: "In this post, we clean up our compiler."
|
||||||
---
|
---
|
||||||
|
|
||||||
|
|
|
@ -1,6 +1,7 @@
|
||||||
---
|
---
|
||||||
title: "Multiple Typeclass Instances using Newtype in Haskell"
|
title: "Multiple Typeclass Instances using Newtype in Haskell"
|
||||||
date: 2022-04-28T23:09:42-07:00
|
date: 2022-04-28T23:09:42-07:00
|
||||||
|
expirydate: 2022-04-28T23:09:42-07:00
|
||||||
tags: ["Haskell"]
|
tags: ["Haskell"]
|
||||||
draft: true
|
draft: true
|
||||||
---
|
---
|
||||||
|
|
|
@ -1,6 +1,7 @@
|
||||||
---
|
---
|
||||||
title: "Induction Principles from Base Functors"
|
title: "Induction Principles from Base Functors"
|
||||||
date: 2022-04-22T12:19:22-07:00
|
date: 2022-04-22T12:19:22-07:00
|
||||||
|
expirydate: 2022-04-22T12:19:22-07:00
|
||||||
tags: ["Idris"]
|
tags: ["Idris"]
|
||||||
draft: true
|
draft: true
|
||||||
---
|
---
|
||||||
|
|
|
@ -1,6 +1,7 @@
|
||||||
---
|
---
|
||||||
title: Typeclasses are Basically Logic Programming
|
title: Typeclasses are Basically Logic Programming
|
||||||
date: 2021-06-28T17:11:38-07:00
|
date: 2021-06-28T17:11:38-07:00
|
||||||
|
expirydate: 2021-06-28T17:11:38-07:00
|
||||||
draft: true
|
draft: true
|
||||||
description: "In this post, we explore the connection between typeclasses and logic programming."
|
description: "In this post, we explore the connection between typeclasses and logic programming."
|
||||||
tags: ["Haskell", "Prolog"]
|
tags: ["Haskell", "Prolog"]
|
||||||
|
|
|
@ -2,6 +2,7 @@
|
||||||
title: Meaningfully Typechecking a Language in Idris
|
title: Meaningfully Typechecking a Language in Idris
|
||||||
date: 2020-02-27T21:58:55-08:00
|
date: 2020-02-27T21:58:55-08:00
|
||||||
tags: ["Haskell", "Idris", "Programming Languages"]
|
tags: ["Haskell", "Idris", "Programming Languages"]
|
||||||
|
series: "Meaningfully Typechecking a Language in Idris"
|
||||||
---
|
---
|
||||||
|
|
||||||
This term, I'm a TA for Oregon State University's Programming Languages course.
|
This term, I'm a TA for Oregon State University's Programming Languages course.
|
||||||
|
|
|
@ -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", "Programming Languages"]
|
tags: ["Idris", "Programming Languages"]
|
||||||
|
series: "Meaningfully Typechecking a Language in Idris"
|
||||||
favorite: true
|
favorite: true
|
||||||
---
|
---
|
||||||
|
|
||||||
|
|
|
@ -2,6 +2,7 @@
|
||||||
title: Meaningfully Typechecking a Language in Idris, With Tuples
|
title: Meaningfully Typechecking a Language in Idris, With Tuples
|
||||||
date: 2020-08-12T15:48:04-07:00
|
date: 2020-08-12T15:48:04-07:00
|
||||||
tags: ["Idris", "Programming Languages"]
|
tags: ["Idris", "Programming Languages"]
|
||||||
|
series: "Meaningfully Typechecking a Language in Idris"
|
||||||
---
|
---
|
||||||
|
|
||||||
Some time ago, I wrote a post titled
|
Some time ago, I wrote a post titled
|
||||||
|
|
6
content/series/_index.md
Normal file
6
content/series/_index.md
Normal file
|
@ -0,0 +1,6 @@
|
||||||
|
---
|
||||||
|
title: "Series"
|
||||||
|
---
|
||||||
|
Sometimes, content about the same topic is best organized into multiple posts.
|
||||||
|
The following series span multiple articles, but have a common overarching
|
||||||
|
theme.
|
10
content/series/a-language-for-an-assignment/_index.md
Normal file
10
content/series/a-language-for-an-assignment/_index.md
Normal file
|
@ -0,0 +1,10 @@
|
||||||
|
+++
|
||||||
|
title = "A Language for an Assignment"
|
||||||
|
summary = """
|
||||||
|
In this series, I create a brand new programming language for each homework
|
||||||
|
assignment of my algorithms class. I try to make the language whimsical
|
||||||
|
and specialized to only the problem at hand. The languages are implemented
|
||||||
|
using Haskell, and translate to Python.
|
||||||
|
"""
|
||||||
|
status = "suspended"
|
||||||
|
+++
|
9
content/series/advent-of-code-in-coq/_index.md
Normal file
9
content/series/advent-of-code-in-coq/_index.md
Normal file
|
@ -0,0 +1,9 @@
|
||||||
|
+++
|
||||||
|
title = "Advent of Code in Coq"
|
||||||
|
summary = """
|
||||||
|
In this series, I apply the Coq proof assistant to formalize solutions to the
|
||||||
|
puzzles to Advent of Code 2020. That is, I try to solve the problem, and
|
||||||
|
formally prove that the solution is correct.
|
||||||
|
"""
|
||||||
|
status = "suspended"
|
||||||
|
+++
|
|
@ -0,0 +1,11 @@
|
||||||
|
+++
|
||||||
|
title = "Compiling a Functional Language using C++"
|
||||||
|
summary = """
|
||||||
|
This series covers the implementation of a compiler for a lazily evaluated
|
||||||
|
functional language using C++ and LLVM. The language is initially based on
|
||||||
|
my project for a university course in compilers, but is extended with many
|
||||||
|
additional features, such as polymorphism, let-in expressions, and
|
||||||
|
polymorphism.
|
||||||
|
"""
|
||||||
|
status = "complete"
|
||||||
|
+++
|
10
content/series/everything-i-know-about-types/_index.md
Normal file
10
content/series/everything-i-know-about-types/_index.md
Normal file
|
@ -0,0 +1,10 @@
|
||||||
|
+++
|
||||||
|
title = "Everything I Know About Types"
|
||||||
|
summary = """
|
||||||
|
In this series, I try to write down and organize all I know about type systems.
|
||||||
|
Most of this knowledge was acquired over my time as a researcher in the field
|
||||||
|
of programming languages at Oregon State University.
|
||||||
|
"""
|
||||||
|
status = "ongoing"
|
||||||
|
draft = true
|
||||||
|
+++
|
|
@ -0,0 +1,11 @@
|
||||||
|
+++
|
||||||
|
title = "Meaningfully Typechecking a Language in Idris"
|
||||||
|
summary = """
|
||||||
|
In this series, I use the dependently-typed programming language Idris to
|
||||||
|
implement relatively simple typechecking of a simple object language.
|
||||||
|
However, I do so with a twist: the typechecker produces expressions
|
||||||
|
that are guaranteed to be safe to evaluate. The interpreter then
|
||||||
|
doesn't have to worry about checking for type errors.
|
||||||
|
"""
|
||||||
|
status = "complete"
|
||||||
|
+++
|
|
@ -1 +1 @@
|
||||||
Subproject commit e7cada3764d9700e9d29134bc07571cc29d1572f
|
Subproject commit e431d65659148919ae8c60d1c1873abd039c40be
|
Loading…
Reference in New Issue
Block a user