All pages
From The Twelf Project
| All pages | Next page (Summer school 2008:Arithmetic expressions with pairs (value)) |
- %.
- %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
- CADE Tutorial
- CADE Tutorial/Basic error messages
- CADE Tutorial/Basics
- CADE Tutorial/Basics Answer
- CADE Tutorial/Combinators
- CADE Tutorial/Combinators Answer
- CADE Tutorial/Combinators Support
- CADE Tutorial/MinML
- CADE Tutorial/MinML Answer
- CADE Tutorial/MinML encoding
- CADE Tutorial/Next
- 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)
