brendanzab

(** An elaborator for a simply typed lambda calculus with mutable metavars.

    This implementation is based on Arad Arbel’s gist:
    https://gist.github.com/aradarbel10/837aa65d2f06ac6710c6fbe479909b4c
*)

module Core = struct

  (** {1 Types} *)

brendanzab

module IndexedMonad = struct

  module type S = sig

    type ('i, 'a) t

    val pure : 'a -> (_, 'a) t
    val bind : ('i, 'a) t -> ('a -> ('i, 'b) t) -> ('i, 'b) t

  end

brendanzab

Functional, Reactive, and Distributed Systems Bibliography

Books

• CQRS Journey: Free ebook from Microsoft (Print book available for purchase)
• Functional and Reactive Domain Modeling: A high level overview of how to build up domain models using free monads and interpreters.
• Reactive Microservices Architecture: Free booklet from Lagom and O'Reilly
• Reactive Messaging Patterns with the Actor Model: Applications and Integration in Scala and Akka
• Domain-Driven Design: Tackling Complexity in the Heart of Software

brendanzab

(** {0 Elaboration with Record Patching and Singleton Types}

    This is a small implementation of a dependently typed language with
    dependent record types, with some additional features intended to make it
    more convenient to use records as first-class modules. It was originally
    ported from {{: https://gist.github.com/mb64/04315edd1a8b1b2c2e5bd38071ff66b5}
    a gist by mb64}.

    The type system is implemented in terms of an ‘elaborator’, which type
    checks and tanslates a user-friendly surface language into a simpler and

brendanzab

(** {0 An implementation of a small dependently typed language}

    This is an implementation simple dependently typed language where types are
    first-class and where the output types of functions may depend on the inputs
    supplied to them.

    Type checking is is implemented in terms of an {i elaborator}, which checks
    and tanslates a user-friendly {i surface language} into a simpler and more
    explicit {i core language} that is more closely connected to type theory.
    Because we need to simplify types during elaboration we also implement an

brendanzab

[{"tag":"Heading","contents":[0,"Martin-Löf Type Theory"]},{"tag":"Paragraph","contents":"A description of Martin-Löf Type Theory in Holbert, by Brendan Zabarauskas."},{"tag":"Paragraph","contents":"Original gist: ~https://gist.github.com/brendanzab/1b4732179b15201bf33fed6dbca02458~"},{"tag":"Heading","contents":[2,"Introduction"]},{"tag":"Paragraph","contents":"/Martin-Löf Type Theory/ (MLTT), also known as /Intuitionistic Type Theory/, is a type theory proposed by Per Martin-Löf in the mid 70s. It forms the basis of many popular dependently typed programming languages and theorem provers, for example Agda, Coq, Idris, Epigram, and more. The influence of MLTT also extends to other languages, for example partly inspiring the module systems of Standard ML and OCaml, and in the work on adding dependent types to Haskell."},{"tag":"Paragraph","contents":"The main forms of judgement in this presentation of Martin-Löf Type theory are:\n\n- $A:_type A$\n    which can be read as “$A:A$ is a type”\n\n- $A a:_:_ a A$\n

brendanzab

Prototyping Rust Code in CodeRunner

CodeRunner is a nifty little app for OSX that allows you to play around with test code with minimal fuss. Here are some instructions for setting it up to build Rust code.

Setup instructions

1. Go to CodeRunner > Preferences...
2. Select the Languages tab

brendanzab

Inference Rules

Natural deduction

T ::=
  | Int
  | Bool

t1, t2 ::=

brendanzab

System λ

The untyped lambda calculus

e ::=             terms:
  x               variable
  e e             application
  λ x . e         abstraction

brendanzab

/-
  A proof of the correctness of an arithmetic expression compiler in Lean 4.

  Ported from [expcompile.v], which is part of Derek Dreyer and Gert Smolka's
  [course material].

  [expcompile.v]: https://www.ps.uni-saarland.de/courses/sem-ws17/expcompile.v
  [course material]: https://courses.ps.uni-saarland.de/sem_ws1718/3/Resources
-/