All pages

From The Twelf Project

%.	%assert	%block
%clause	%covers	%establish
%freeze	%infix	%mode
%name	%postfix	%prefix
%prove	%query	%querytabled
%reduces	%solve	%subord
%tabled	%terminates	%thaw
%theorem	%total	%trustme
%unique	%use	%worlds
Abbrev declaration	About The Twelf Project	Abstract syntax
Ad hoc binding structures	Adequacy	Adequate
Admissibility of cut	Alpha-equivalence	Ambiguous hyperkind
Ask Twelf Elf	Ask Twelf Elf:Short Answers	Ask Twelf Elf:Short answers
Auto-freezing	Autofreeze	Beta-equivalence
Beta-equivalent	Beta-normal	Beta-reduction
Beta equivalence	Beta equivalent	Bibliography of LF
Block	Blocks	CPS conversion
Canonical form	Canonical forms	Canonical forms lemma
Case studies	Catch-all case	Church-Rosser via Complete Development
Church-Rosser via complete development	Classical S5	Compatibility lemma
Compositional bijection	Concrete representation	Concrete representations
Congruence lemma	Congruence lemmas	Congruence relation
Constraint domain	Constraint domains	Constraint domains and coverage checking
Converting between implicit and explicit parameters	Correctness of mergesort	Coverage checking
Cut	Cut elimination	Debugging coverage errors
Deductive system	Deductive systems	Deep equality
Define declaration	Dense lexicographical orderings	Dependent type
Dependent types	Deterministic declaration	Developers
Division over the natural numbers	Documentation	Download
Editing Summer school 2008:Alternate typed arithmetic expressions with sums	Effectiveness	Effectiveness lemma
Effectiveness lemmas	Equality	Equivalence relation
Equivalence relations	Error messages	Eta-equivalence
Eta-expansion	Eta-long	Eta-long form
Exchange	Exchange lemma	Explicit context
Explicit parameter	Extrinsic encoding	Factoring
Fixity declaration	Focusing	Freeze
Frozen	Function	Function (relation)
General Description of Twelf	General description of Twelf	Glossary
Ground	HOAS nat bijection	Hauptsatz
Hereditary substitution	Hereditary substitution for the STLC	Hereditary substitution for the STLC (part 2)
Heterogeneous lists	Higher-order abstract syntax	Higher-order judgement
Higher-order judgements	Higher-order judgment	Higher-order judgments
Holes in metatheorems	Homogeneous lists	Hypothetical judgement
Hypothetical judgment	Identity	Implicit and explicit parameters
Implicit parameter	Implicit parameters	Incremental metatheorem development
Indexed HOAS nat bijection	Indexed lists	Input coverage
Intrinsic and extrinsic encodings	Intrinsic encoding	Introductions to Twelf
Judgement	Judgment	Judgments
Judgments as types	LF	Language with references
Letrec	Lexicographical orderings with density	Lily
Linear logic	Lists	Logic program
Logic programming	Mailing lists	Main Page
Main page	Manipulating proof witnesses	Manipulating proof witnesses as inputs
Meta-language	Meta-logic	Metatheorem
Metatheorems	Mode	Mode checking
Modes of use	Mutable state	Mutual induction
Naming conventions	Natural number	Natural numbers
Natural numbers with inequality	Negation as failure	Numeric termination metric
Numeric termination metrics	Object language	Object logic
Object logic syntax	Output coverage	Output factoring
Output freeness	PLTheory:Introduction to Twelf	Pattern Matching (Case Study)
Pattern matching	Programming language theory with Twelf	Progress
Proofs by reductio ad absurdum	Proving metatheorems with Twelf	Quick introduction
Real-world binding structures	Real World Binding Structures	Reasoning from equality
Reasoning from false	Reformulating languages to use hypothetical judgements	Regular world
Regular worlds	Relation	Release history
Research projects using Twelf	Respects lemma	Respects lemmas
Revision history	Sets and supersets	Shallow equality
Signature	Simplifying dynamic clauses	Simply-typed lambda calculus
Software	Strengthening	Structural metric
Structural metrics	Structural termination metrics	Style guide
Subordination	Substitution	Substitution Lemma
Substitution lemma	Sudoku	Summer school 2008
Summer school 2008:Alternate typed arithmetic expressions with sums	Summer school 2008:Arithmetic expressions	Summer school 2008:Arithmetic expressions with call-by-value let-binding
Summer school 2008:Arithmetic expressions with let-binding	Summer school 2008:Arithmetic expressions with let-binding (hypothetical evaluation)	Summer school 2008:Arithmetic expressions with pairs (value)
Summer school 2008:Encoding of System F	Summer school 2008:Exercises 1	Summer school 2008:Exercises 2
Summer school 2008:Exercises 3	Summer school 2008:Type safety for MinML (extrinsic encoding)	Summer school 2008:Type safety for MinML (intrinsic encoding)
Summer school 2008:Type safety for MinML with monadic effects	Summer school 2008:Type safety for MinML with monadic effects (putngetn)	Summer school 2008:Type safety for polymorphic MinML (intrinsic encoding)
Summer school 2008:Typed arithmetic expressions	Summer school 2008:Typed arithmetic expressions (extrinsic encoding)	Summer school 2008:Typed arithmetic expressions (value)
Summer school 2008:Typed arithmetic expressions with pairs	Summer school 2008:Typed arithmetic expressions with sums	Summer school 2008:Typed arithmetic expressions with sums 2
Summer school 2008: Exercise: Typed arithmetic expressions with pairs	Syntax (Object logic)	Tabled logic programming
Tactical theorem proving	Termination analysis	The two Twelfs
Theorem prover	Totality assertion	Totality assertions
Try Twelf now	Tutorial	Tutorials
Twelf-list	TwelfTag	Twelf Elf Rotation Charter
Twelf Live	Twelf glossary	Twelf naming conventions
Twelf signature	Twelf style guide	Twelf with Emacs
Twelf without Emacs	Type families	Type family
Unary numbers	Unification	Uniqueness lemma
Uniqueness lemmas	Universal quantification	Universally quantified
Unsafe mode	User's Guide	User-defined constraint domain
Using a metric	Using nat-less with %reduces	Weakening
Weakening lemma	What's new	What's new?
Working with higher-order judgements	World	World subsumption
Zermelo Frankel	Β-equivalence	Β equivalence

Retrieved from "http://twelf.plparty.org/wiki/Special:Allpages"

All pages

From The Twelf Project

Views

Personal tools

the twelf wiki

learn twelf

reference

Search

Toolbox