lastland
Assistant Professor at Portland State University. Functional Programming. Formal Verification. Haskell/Coq.
Portland State UniversityPortland, OR
Pinned Repositories
ClairvoyanceMonad
The Coq formalization of the paper Reasoning about the garden of forking paths.
DTScala
Dependent Types in Scala
HaskellTheoremProver
A theorem proving framework for intuitionistic and classical propositional logics in Haskell.
MINIX-3.1.7-Lottery-Scheduler
A patch to implement lottery scheduling policy on MINIX 3.1.7.
scala-forklift
Type-safe data migration tool for Slick, Git and beyond.
Tricks-Museum
a collection for interesting code tricks
WebSpec
hs-to-coq
Convert Haskell source code to Coq source code.
QuickChick
Randomized Property-Based Testing Plugin for Coq
lastland's Repositories
lastland/scala-forklift
Type-safe data migration tool for Slick, Git and beyond.
lastland/ClairvoyanceMonad
The Coq formalization of the paper Reasoning about the garden of forking paths.
lastland/play-slick-forklift-example
An example of doing database migration using play, play-slick, and scala-forklift.
lastland/PTSemForEffects
A Coq formalization of the paper "A Predicate Transformer Semantics for Effects (Functional Pearl)"
lastland/lastland.github.io
Personal web page.
lastland/my-notes
my notes on books, courses, and others.
lastland/FPInPL
A collection of FP concepts in languages other than traditional functional languages.
lastland/FPScala
lastland/generic-vale
lastland/ProgramAdverbs
The Coq formalization of the paper Program Adverbs and Tlön Embeddings by Yao Li and Stephanie Weirich, published at ICFP 2022.
lastland/coq
Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.
lastland/coq-ghc-base
lastland/FreerArrow
lastland/FStar
Verification system for effectful programs
lastland/GHC-Core-Literature-Review
Literature review of GHC's Core language, System FC
lastland/HasChor
Functional choreographic programming in Haskell
lastland/haskell-ci
Writing CI configurations with Haskell (a better name is needed)
lastland/homebrew-cask
🍻 A CLI workflow for the administration of macOS applications distributed as binaries
lastland/hs-to-coq
Convert Haskell source code to Coq source code
lastland/hs-to-coq-1
Convert Haskell source code to Coq source code.
lastland/hs-to-coq-testbed
lastland/icfp22-layered-monadic-interpreters
artifact for ICFP'22 paper "Formal Reasoning About Layered Monadic Interpreters"
lastland/InteractionTrees
Formalization of the Interaction Tree Datatype in Coq
lastland/ml-for-proofs
An open bibliography of machine learning for formal proof papers
lastland/plclub-web
A Hakyll [plclub] website (https://www.cis.upenn.edu/~plclub/)
lastland/rms-open-letter.github.io
lastland/sail
Sail architecture definition language
lastland/tpchina.github.io
lastland/united
United Monoids
lastland/vellvm
The Vellvm (Verified LLVM) coq development.