SASyLF (pronounced "Sassy Elf") is an LF-based proof assistant specialized to checking theorems about programming languages and logics. SASyLF has a simple design philosophy: language and logic syntax, semantics, and meta-theory should be written as closely as possible to the way it is done on paper. SASyLF can express proofs typical of an introductory graduate type theory course. SASyLF proofs are generally very explicit, but its built-in support for variable binding provides substitution properties for free and avoids awkward variable encodings.

Project Samples

SASyLF 1.2.4 Quick Fix SASyLF 1.3.0 Packages

Project Activity

See All Activity >

Follow SASyLF

SASyLF Web Site

Other Useful Business Software
Train ML Models With SQL You Already Know Icon
Train ML Models With SQL You Already Know

BigQuery automates data prep, analysis, and predictions with built-in AI assistance.

Build and deploy ML models using familiar SQL. Automate data prep with built-in Gemini. Query 1 TB and store 10 GB free monthly.
Start Free
Rate This Project
Login To Rate This Project

User Reviews

Be the first to post a review of SASyLF!

Additional Project Details

User Interface

Eclipse

Registered

2013-08-15
Report inappropriate content