All Projects → TiarkRompf → Collapsing Towers

TiarkRompf / Collapsing Towers

Collapsing Towers of Interpreters

Labels

Projects that are alternatives of or similar to Collapsing Towers

Jt89
sn76489an compatible Verilog core, with emphasis on FPGA implementation and Megadrive/Master System compatibility
Stars: ✭ 14 (-77.05%)
Mutual labels:  coq
Compcert
The CompCert formally-verified C compiler
Stars: ✭ 984 (+1513.11%)
Mutual labels:  coq
Metalib
The Penn Locally Nameless Metatheory Library
Stars: ✭ 47 (-22.95%)
Mutual labels:  coq
Vvclocks
Verified vector clocks, with Coq!
Stars: ✭ 14 (-77.05%)
Mutual labels:  coq
Nuprlincoq
Implementation of Nuprl's type theory in Coq
Stars: ✭ 31 (-49.18%)
Mutual labels:  coq
Certint
A Certified Interpreter for ML with Structural Polymorphism
Stars: ✭ 39 (-36.07%)
Mutual labels:  coq
Stalin Sort
Add a stalin sort algorithm in any language you like ❣️ if you like give us a ⭐️
Stars: ✭ 868 (+1322.95%)
Mutual labels:  coq
Perennial
Verifying concurrent crash-safe systems
Stars: ✭ 57 (-6.56%)
Mutual labels:  coq
Paramcoq
Coq plugin for parametricity [[email protected]]
Stars: ✭ 32 (-47.54%)
Mutual labels:  coq
Poleiro
A blog about Coq
Stars: ✭ 42 (-31.15%)
Mutual labels:  coq
Coq Printf
Implementation of sprintf for Coq
Stars: ✭ 15 (-75.41%)
Mutual labels:  coq
Profunctor Monad
Bidirectional programming in Haskell with monadic profunctors
Stars: ✭ 30 (-50.82%)
Mutual labels:  coq
Freespec
A framework for implementing and certifying impure computations in Coq
Stars: ✭ 41 (-32.79%)
Mutual labels:  coq
Hello World
A Hello World program in Coq.
Stars: ✭ 14 (-77.05%)
Mutual labels:  coq
Silveroak
Formal specification and verification of hardware, especially for security and privacy.
Stars: ✭ 51 (-16.39%)
Mutual labels:  coq
Ledgertheory
Stars: ✭ 12 (-80.33%)
Mutual labels:  coq
Parseque
Total Parser Combinators in Coq
Stars: ✭ 37 (-39.34%)
Mutual labels:  coq
Scala Escape
A compiler plug-in to control object lifetimes in Scala
Stars: ✭ 60 (-1.64%)
Mutual labels:  coq
Verlang
Stars: ✭ 52 (-14.75%)
Mutual labels:  coq
Pornview
Porn browser formally-verified in Coq
Stars: ✭ 42 (-31.15%)
Mutual labels:  coq

Collapsing Towers of Interpreters

We are concerned with the following challenge: given a sequence of programming languages L_0,...,L_n and interpreters for L_i+1 written in L_i, derive a compiler from L_n to L_0. This compiler should be one-pass, and it should be optimal in the sense that the translation removes all interpretive overhead of the intermediate languages.

See popl18 directory for the authorative artifact accompanying the POPL 2018 paper Collapsing Towers of Interpreters.

Note that the project description data, including the texts, logos, images, and/or trademarks, for each open source project belongs to its rightful owner. If you wish to add or remove any projects, please contact us at [email protected].