SASyLF

SASyLF is an proof assistant for reasoning about programs.

Brought to you by: boyland, jonathanaldrich

Downloads: 0 This Week

Last Update: 2016-09-21

Get an email when there's a new version of SASyLF

Windows Mac Linux BSD ChromeOS

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

Keep company data safe with Chrome Enterprise Icon

Keep company data safe with Chrome Enterprise

Protect your business with AI policies and data loss prevention in the browser

Make AI work your way with Chrome Enterprise. Block unapproved sites and set custom data controls that align with your company's policies.

Download Chrome

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

Recommended Projects

Agda
Agda is a dependently typed, total functional programming language and interactive theorem prover based on Martin-Löf’s type theory. It allows expressing programs and proofs in the same language, using the Curry–Howard correspondence. It features interactive development via Emacs, Atom, or VS...
HLM Proof Assistant
HLM is a proof assistant for everyday mathematics, which is currently being developed. It aims for a user experience as close as possible to regular mathematical practice, and proofs which are understandable by humans with little extra effort.
DeepSeek Prover V2
DeepSeek-Prover-V2 is DeepSeek’s specialized model for formal theorem proving, particularly targeting proof in Lean 4. The repository describes how they use recursive proof decomposition by prompting DeepSeek-V3 to break complex theorems into subgoals, synthesize proof sketches, and then combine...
Lean Copilot
LeanCopilot integrates large language models (LLMs) as copilots for theorem proving in the Lean proof assistant. It assists users by suggesting tactics, premises, and searching for proofs, thereby enhancing the efficiency of formal verification processes. LeanCopilot supports both built-in...
Natural Deduction Planner
This application aids in the creation of Natural Deduction style logical proofs. The style is that used in University of Auckland Philosophy courses. Upon inputting a sequent, a proof can be completed within Natural Deduction Planner. The result can be exported to png, to text or to LaTeX macros.