Comments (4)
Working on getting this into L1IR.
from lsts.
Codegen should move from cranelift to new project Lambda Mountain. It will be nice to have a backend that is built to support functional programming. In the meantime we can quickly run up an interpreted version of LM which shouldn't take too long to develop and can support lots of random functionality.
L1IR is still useful to provide an interface for bridging the polymorphic/monomorphic divide as well as generating policies for LM.
from lsts.
LM is probably better suited to bridge the polymorphic/monomorphic divide. Let's just jump straight into LM from the backend.
from lsts.
Interpreter is not JIT compiled yet but it all gets the same interface in the end. Finally LSTS can wash its hands of implementation details and just focus on proofs.
from lsts.
Related Issues (20)
- Introduce
- Introduce "Zero" at the type level
- Write unification algorithm in L1 HOT 1
- Update Tutorial
- Generate documentation for each prelude
- Target Rust for AoT compilation HOT 2
- Integrate Constraint Solver in type system HOT 1
- Integration objective functions to type system HOT 1
- Make signed integers the default number literal
- Replace Regexes with DFAs
- Formal verification with stronger logical kernel HOT 2
- Cannot run the basic example of LSTS HOT 5
- Migrate backend to LM HOT 1
- Simple Compiler targeting LLVM IR HOT 9
- Start bootstrapping l1 in l1 HOT 1
- Contemplate relaxing the one datatype per type restriction HOT 1
- Formalize Type System Inference HOT 3
- Isolate type rules for conjunction types HOT 2
- Benchmark Auto Theorems
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from lsts.