Edinburgh Logical Framework

37

ENTCS
2008

101views more ENTCS 2008»

Normalization for the Simply-Typed Lambda-Calculus in Twelf

13 years 11 months ago

Normalization for the simply-typed -calculus is proven in Twelf, an implementation of the Edinburgh Logical Framework. Since due to proof-theoretical restrictions Twelf Tait'...

Andreas Abel

claim paper

Read More »

33

click to vote

ENTCS
2008

101views more ENTCS 2008»

Imperative LF Meta-Programming

13 years 11 months ago

Download www.cs.yale.edu

Logical frameworks have enjoyed wide adoption as meta-languages for describing deductive systems. While the techniques for representing object languages in logical frameworks are ...

Aaron Stump

claim paper

Read More »

29

click to vote

LICS
1987
IEEE

75views Automated Reasoning» more LICS 1987»

A Framework for Defining Logics

14 years 2 months ago

Download homepages.inf.ed.ac.uk

The Edinburgh Logical Framework (LF) provides a means to define (or present) logics. It is based on a general treatment of syntax, rules, and proofs by means of a typed -calculus ...

Robert Harper, Furio Honsell, Gordon D. Plotkin

claim paper

Read More »

Sciweavers

Explore & Download

Productivity Tools

Document Tools

Image Tools

Sciweavers