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

Project Activity

See All Activity >

Follow SASyLF

SASyLF Web Site

Other Useful Business Software
Your top-rated shield against malware and online scams | Avast Free Antivirus Icon
Your top-rated shield against malware and online scams | Avast Free Antivirus

Browse and email in peace, supported by clever AI

Our antivirus software scans for security and performance issues and helps you to fix them instantly. It also protects you in real time by analyzing unknown files before they reach your desktop PC or laptop — all for free.
Free Download
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