All pages with prefix

From The Twelf Project

All pages Display pages with prefix: Namespace: (Main) Talk User User talk The Twelf Project The Twelf Project talk File File talk MediaWiki MediaWiki talk Template Template talk Help Help talk Category Category talk Elves Elves talk Proving metatheorems Proving metatheorems talk

All pages | Next page (Summer school 2008:Typed arithmetic expressions (extrinsic encoding))

%.	%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
Big algebraic solver	Block	Blocks
Bracket abstraction	CPS conversion	C machine and focusing
C machine and focusing (composition in machine state)	C machine and focusing (internalized compositon)	Canonical form
Canonical forms	Canonical forms lemma	Case studies
Catch-all case	Church-Rosser (w/ catch-all case)	Church-Rosser (w/ identity reduction)
Church-Rosser via Complete Development	Church-Rosser via complete development	Classical S5
Compatibility lemma	Compositional bijection	Computation and Deduction 2009
Computation and Deduction 2009/20090203	Computation and Deduction 2009/20090204	Computation and Deduction 2009/20090209
Computation and Deduction 2009/20090223	Computation and Deduction 2009/20090304	Computation and Deduction 2009/20090304-support
Computation and Deduction 2009/20090316	Computation and Deduction 2009/20090318	Computation and Deduction 2009/20090325
Computation and Deduction 2009/20090330	Computation and Deduction 2009/20090401	Computation and Deduction 2009/20090406
Computation and Deduction 2009/20090408	Computation and Deduction 2009/20090413	Computation and Deduction 2009/20090415
Computation and Deduction 2009/20090420	Computation and Deduction 2009/20090422	Computation and Deduction 2009/20090427
Computation and Deduction 2009/20090429	Computation and Deduction 2009/Test Page 1	Concrete representation
Concrete representations	Congruence lemma	Congruence lemmas
Congruence relation	Constraint domain	Constraint domains
Constraint domains and coverage checking	ConstructiveSemantics	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	Double-negation translation	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
Evaluation contexts	Exchange	Exchange lemma
Explicit context	Explicit parameter	Extrinsic encoding
Factoring	First-order encodings	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)	Hereditary substitution with a zipper
Hereditary substitution with zippers	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	Iterated Let Bindings	Iterated inductive definitions and defunctionalization
Judgement	Judgment	Judgments
Judgments as types	LF	Language with references
Lax logic	Let*	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	MediaWiki formatting description
Meta-language	Meta-logic	Metatheorem
Metatheorems	MinMLToMinHaskell	Modal logic
Modally Propositional Logic	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	POPL Tutorial
POPL Tutorial/Basic error messages	POPL Tutorial/Basics	POPL Tutorial/Basics Answer
POPL Tutorial/Basics Starter	POPL Tutorial/Big step, small step	POPL Tutorial/Big step, small step: Solution
POPL Tutorial/CPS	POPL Tutorial/CPS Solution2	POPL Tutorial/CPS Solutions
POPL Tutorial/Church Rosser	POPL Tutorial/Church Rosser (Problem)	POPL Tutorial/Combinators
POPL Tutorial/Combinators (karl)	POPL Tutorial/Combinators Answer	POPL Tutorial/Combinators Starter
POPL Tutorial/Combinators Support	POPL Tutorial/Combinators session	POPL Tutorial/Combinators session (answers)
POPL Tutorial/Control machine	POPL Tutorial/Cost Semantics	POPL Tutorial/Cost semantics
POPL Tutorial/Evaluation Contexts Intrinsic	POPL Tutorial/Exceptions	POPL Tutorial/Exceptions-problem
POPL Tutorial/MinML	POPL Tutorial/MinML Answer	POPL Tutorial/MinML Encoding
POPL Tutorial/MinML Preservation Theorem	POPL Tutorial/MinML Preservation Theorem: Solution	POPL Tutorial/MinML Preservation Theorem Answer
POPL Tutorial/MinML Starter	POPL Tutorial/MinML encoding	POPL Tutorial/Nat
POPL Tutorial/Nat Starter	POPL Tutorial/New language	POPL Tutorial/Next
POPL Tutorial/Pattern Matching	POPL Tutorial/Pattern matching	POPL Tutorial/Problems
POPL Tutorial/Properties of Typing and Reduction	POPL Tutorial/Saturday	POPL Tutorial/Sequent vs Natural Deduction
POPL Tutorial/Sequent vs Natural Deduction: Solution	POPL Tutorial/Session2	POPL Tutorial/Session 2
POPL Tutorial/Session 2 Answer	POPL Tutorial/Session 2 Script	POPL Tutorial/Session 2 Starter
POPL Tutorial/Session 4	POPL Tutorial/Session 4 Answer	POPL Tutorial/Session 4 Live
POPL Tutorial/Session 4 Starter	POPL Tutorial/Session 5	POPL Tutorial/Thursday
POPL Tutorial/Typed bracket abstraction	POPL Tutorial/Typed bracket abstraction (solution)	POPL Tutorial/Typed bracket abstraction with equivalence
POPL Tutorial/cps	POPL Tutorial/cps-ctp	POPL Tutorial/cps-problem
POPL Tutorial/cps-problem2	POPL Tutorial/cps-rp	POPL Tutorial/cps-truefalse
Pattern Matching (Case Study)	Pattern matching	Polarized PCF
Polarized PCF Better	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	Signature checking	Signatures as logic programs
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