Copyright © 1998, 2000, 2002 Frank Pfenning and Carsten Schuermann
[ << ] | [ < ] | [ Up ] | [ > ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
1 Introduction | Getting started | |
2 Lexical Conventions | Reserved characters and identifiers | |
3 Syntax | Grammar of signatures | |
4 Term Reconstruction | Checking and inferring types | |
5 Logic Programming | How to interpret signatures as programs | |
6 Constraint Domains | Using rationals and integers | |
7 Modes | Input/output behavior of relations | |
8 Termination | Verifying termination of programs | |
9 Coverage | Checking that all cases are covered | |
10 Theorem Prover | Proving theorems and meta-theorems | |
11 ML Interface | Running Twelf from ML | |
12 Twelf Server | A stand-alone Twelf command interpreter | |
13 Emacs Interface | Editing Twelf files | |
14 Installation | How to install Twelf | |
15 Examples | Guide to standard examples | |
16 History | Differences between Elf 1.5 and Twelf | |
Index | Index to this guide | |
— The Detailed Node Listing — Introduction | ||
---|---|---|
1.1 New Features | Differences from Twelf 1.2 | |
1.2 Quick Start | Sample interaction with Twelf | |
Lexical Conventions | ||
2.1 Reserved Characters | Characters separating identifiers | |
2.2 Identifiers | Interpretation of identifiers | |
Syntax | ||
3.1 Grammar | The grammar of Twelf | |
3.2 Constructor Declaration | Introducing types and object constructors | |
3.3 Definitions | Notational definitions and abbreviations | |
3.4 Operator Declaration | Infix, prefix and postfix operators | |
3.5 Name Preferences | Assigning names to anonymous variables | |
3.6 Sample Signature | Example of First-Order Logic | |
Term Reconstruction | ||
4.1 Implicit Quantifiers | Free variables in declarations | |
4.2 Implicit Arguments | Omitted arguments to constants | |
4.3 Strict Occurrences | A sufficient condition for principal types | |
4.4 Strict Definitions | Reconstruction on definitions | |
4.5 Type Ascription | Disambiguating terms | |
4.6 Error Messages | When things go wrong | |
4.7 Tracing Reconstruction | Seeing what happens during reconstruction | |
Logic Programming | ||
5.1 Query Declaration | Checking expected numbers of solutions | |
5.2 Solve Declaration | Naming proof terms found by search | |
5.3 Interactive Queries | Twelf’s interactive top-level | |
5.4 Sample Trace | An example how search works | |
5.5 Operational Semantics | How queries are executed in some detail | |
5.6 Sample Program | Type inference for a lambda-calculus | |
5.7 Clause Definitions | How to use definitions for search | |
5.8 Deterministic Type Families | How to prune unwanted solutions | |
5.9 Tabled Logic Programming | Executing queries with memo tables | |
Constraint Domains | ||
6.1 Installing an Extension | Making constraint domains available | |
6.2 Equalities over Rational Numbers | Rationals with equality | |
6.3 Inequalities over Rational Numbers | Rationals with equality and inequality | |
6.4 Integer Constraints | Integers with equality and inequality | |
6.5 Equalities over Strings | Strings and concatenation | |
6.6 32-bit Integers | Integers representable as string of 32 bits | |
6.7 Sample Constraint Programs | Some examples of use | |
6.8 Restrictions and Caveats | Alerts! | |
Modes | ||
7.1 Short Mode Declaration | Common form for modes | |
7.2 Full Mode Declaration | Fully explicit modes | |
7.3 Mode Checking | Checking mode correctness | |
Termination | ||
8.1 Termination Declaration | Checking termination | |
8.2 Reduction Declaration | Checking outputs are smaller than inputs | |
8.3 Subterm Ordering | Higher-order subterms | |
8.4 Lexicographic Orders | Termination by nested induction | |
8.5 Simultaneous Orders | Termination by simultaneous induction | |
8.6 Mutual Recursion | Termination of mutually recursive predicates | |
Coverage | ||
9.1 Regular Worlds | Characterizing parameters and hypotheses | |
9.2 Input Coverage | Checking if all cases have been covered | |
9.3 Totality | Verifying if a family is total in its input | |
9.4 Subordination | How constants depend on each other | |
Theorem Prover | ||
10.1 Theorem Declaration | Declaring and proving theorems | |
10.2 Sample Theorems | Two examples | |
10.3 Proof Steps | Basic operations of the prover | |
10.4 Search Strategies | How Twelf searches | |
10.5 Proof Realizations | Using automatically constructed proofs | |
ML Interface | ||
11.1 Configurations | Managing groups of Twelf files | |
11.2 Loading Files | Loading individual files | |
11.3 Environment Parameters | Controlling appearance and verbosity of Twelf | |
11.4 Signature Printing | Printing of signatures | |
11.5 Tracing and Breakpoints | Debugging tools | |
11.6 Timing Statistics | Gathering statistics | |
11.7 Twelf Signature | The top-level signature | |
Twelf Server | ||
12.1 Server Types | Server command argument types | |
12.2 Server Commands | List of Twelf server commands | |
Emacs Interface | ||
13.1 Twelf Mode | Major mode for editing Twelf sources | |
13.2 Editing Commands | Automatic indentation | |
13.3 Type Checking Commands | Checking declarations, files, configurations | |
13.4 Printing Commands | Printing signatures | |
13.5 Tracing Commands | Debugging tools | |
13.6 Error Tracking | Jumping to error locations | |
13.7 Server State | Changing server parameters | |
13.8 Info File | Reading this documentation | |
13.9 Tags Files | Tagging Twelf sources | |
13.10 Twelf Timers | Obtaining runtime statistics from server | |
13.11 Twelf-SML Mode | Running Twelf under SML in Emacs | |
13.12 Emacs Variables | Customizing Twelf mode | |
13.13 Syntax Highlighting | Using multiple fonts for Twelf code | |
13.14 Emacs Initialization | For the .emacs file | |
13.15 Command Summary | Summary of Twelf mode commands | |
Twelf is the current version of a succession of implementations of the logical framework LF. Previous systems include Elf (which provided type reconstruction and the operational semantics reimplemented in Twelf) and MLF (which implemented module-level constructs loosely based on the signatures and functors of ML still missing from Twelf).
Twelf should be understood as research software. This means comments, suggestions, and bug reports are extremely welcome, but there are no guarantees regarding response times. The same remark applies to these notes which constitute the only documentation on the present Twelf implementation.
For current information including download instructions, publications, and mailing list, see the Twelf home page at http://www.cs.cmu.edu/~twelf/. This User’s Guide is published as
Frank Pfenning and Carsten Schuermann Twelf User’s Guide Technical Report CMU-CS-98-173, Department of Computer Science, Carnegie Mellon University, November 1998.
<UL> <LI> <A HREF="http://www.cs.cmu.edu/~twelf/">Twelf Home Page</A> </LI> </UL>
Below we state the typographic conventions in this manual.
code
for Twelf or ML code
for characters and small code fragments
for placeholders in code
for input in verbatim examples
for keystrokes
for mathematical expressions
for emphasized phrases
File names for examples given in this guide are relative to the main
directory of the Twelf installation. For example
‘examples/guide/nd.elf’ may be found in
‘/usr/local/twelf/examples/guide/nd.elf’ if Twelf was installed
into the ‘/usr/local/’ directory.
1.1 New Features | Differences from Twelf 1.2 | |
1.2 Quick Start | Sample interaction with Twelf |
[ << ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
This document was generated on July 9, 2016 using texi2html 5.0.