User contributions
From The Twelf Project
(Latest | Earliest) View (newer 50 | older 50) (20 | 50 | 100 | 250 | 500)
- 10:28, 4 December 2008 (diff | hist) POPL Tutorial/New language (top)
- 18:25, 20 November 2008 (diff | hist) POPL Tutorial/Problems
- 18:23, 20 November 2008 (diff | hist) N POPL Tutorial/Exceptions-problem (New page: %{ Type safety for MinML: call-by-value, with recursive functions, in extrinsic form, with exceptions. In this example, we will take the MinML language from earlier and extend it with co...)
- 17:13, 20 November 2008 (diff | hist) N POPL Tutorial/Exceptions (New page: %{ Type safety for MinML: call-by-value, with recursive functions, in extrinsic form, with exceptions == Syntax == Types: }% tp : type. %name tp T. nat : tp. arr : tp -> tp -> tp. ...)
- 20:02, 17 November 2008 (diff | hist) POPL Tutorial/Problems
- 20:00, 17 November 2008 (diff | hist) POPL Tutorial/cps-rp (top)
- 19:59, 17 November 2008 (diff | hist) N POPL Tutorial/cps-rp (New page: tp : type. o : tp. => : tp -> tp -> tp. %infix right 3 =>. e : tp -> type. v : tp -> type. app : e (A => B) -> e A -> e B. lam : (v A -> e B) -> v (A => B). inj : v A -> e A. %block sourc...)
- 17:54, 17 November 2008 (diff | hist) N POPL Tutorial/Pattern matching (New page: %{ This is a case study on pattern matching using Twelf. }% % nat : type. z : nat. s : nat -> nat. tp : type. o : tp. arrow : tp -> tp -> tp. prod : tp -> tp -> tp. sum : tp -> t...)
- 13:11, 18 October 2007 (diff | hist) N Real-world binding structures (Real-world binding structures moved to Ad hoc binding structures: Ask Karl) (top)
- 13:11, 18 October 2007 (diff | hist) m Ad hoc binding structures (Real-world binding structures moved to Ad hoc binding structures: Ask Karl)
- 20:40, 13 October 2007 (diff | hist) N Letrec (New page: %{ An example of encoding <tt>letrec</tt>, i.e. let-binding a bundle of mutually recursive expressions }% nat : type. z : nat. s : nat -> nat. tp : type. natt : tp. arrow : tp -> tp ...) (top)
- 00:46, 11 October 2007 (diff | hist) Pattern matching
- 20:34, 10 October 2007 (diff | hist) Correctness of mergesort (top)
- 20:32, 10 October 2007 (diff | hist) Correctness of mergesort
- 20:17, 10 October 2007 (diff | hist) User talk:Drl (→Pattern matching scraps (will find a home for these soon))
- 20:16, 10 October 2007 (diff | hist) User talk:Drl (→Pattern matching scraps (will find a home for these soon))
- 17:05, 3 October 2007 (diff | hist) Correctness of mergesort
- 17:03, 3 October 2007 (diff | hist) Correctness of mergesort
- 16:57, 3 October 2007 (diff | hist) Correctness of mergesort
- 16:55, 3 October 2007 (diff | hist) Correctness of mergesort
- 16:54, 3 October 2007 (diff | hist) N Correctness of mergesort (New page: %{ This is an extended example of a proof of mergesort for lists without duplicates. This is an example if showing that an implementation of sorting (mergesort) matches up with a declarati...)
- 15:32, 2 October 2007 (diff | hist) N Negation as failure (New page: %{ Negation as failure. It is possible to do negation-as-failure using Twelf's logic programming engine, with the use of [[%deterministic]]. As an example, we will define logic program...)
- 02:17, 26 March 2007 (diff | hist) Ask Twelf Elf
- 17:38, 19 March 2007 (diff | hist) Explicit context
- 17:38, 19 March 2007 (diff | hist) Explicit context
- 17:18, 19 March 2007 (diff | hist) N Dependent types (New page: A language with '''dependent types''' has types which can mention the terms they classify. For example, LF is a dependently typed language because LF types can mention LF terms. {{st...)
- 17:07, 19 March 2007 (diff | hist) Explicit context
- 17:03, 19 March 2007 (diff | hist) Talk:Glossary
- 16:42, 19 March 2007 (diff | hist) N Explicit context (New page: Explicit contexts are an alternative technique for encoding an object language. Standard practice is to use higher-order abstract syntax in order to implicitly use the LF conte...)
- 16:25, 19 March 2007 (diff | hist) Glossary
- 12:56, 20 October 2006 (diff | hist) Talk:Lists (→Dependent lists)
- 19:06, 16 October 2006 (diff | hist) Tutorials (→Advanced proof techniques)
- 19:05, 16 October 2006 (diff | hist) N Using a metric (Using a metric moved to Structural metrics) (top)
- 19:05, 16 October 2006 (diff | hist) m Structural metrics (Using a metric moved to Structural metrics)
- 19:03, 16 October 2006 (diff | hist) Structural metrics
- 18:43, 16 October 2006 (diff | hist) The Twelf Project:Contributors (→Carnegie Mellon: added Karl)
- 19:29, 15 October 2006 (diff | hist) N The Twelf Project talk:AJALF
- 19:26, 15 October 2006 (diff | hist) What's new
- 19:25, 15 October 2006 (diff | hist) N The Twelf Project:AJALF
- 18:35, 14 October 2006 (diff | hist) Structural metrics (→Using a tree as a metric)
- 17:25, 14 October 2006 (diff | hist) Talk:Ask Twelf Elf
- 17:23, 14 October 2006 (diff | hist) Twelf Elf Rotation Charter (top)
- 17:23, 14 October 2006 (diff | hist) Talk:Ask Twelf Elf (→Current rotation: moving into the charter)
- 17:21, 14 October 2006 (diff | hist) m Twelf Elf Rotation Charter (Protected "Twelf Elf Rotation Charter": don't want people adding random duties (like doing other people's laundry or washing their cars) [edit=sysop:move=sysop])
- 17:19, 14 October 2006 (diff | hist) N Twelf Elf Rotation Charter
- 17:18, 14 October 2006 (diff | hist) Talk:Ask Twelf Elf (→Twelf Elf Rotation Charter)
- 17:17, 14 October 2006 (diff | hist) Talk:Ask Twelf Elf (→Wiki?)
- 17:16, 14 October 2006 (diff | hist) Talk:Ask Twelf Elf (→Twelf Elf E-mail Rotation Charter)
- 21:29, 13 October 2006 (diff | hist) Structural metrics (→Using a tree as a metric)
- 20:30, 13 October 2006 (diff | hist) Talk:Ask Twelf Elf (→Twelf Elf E-mail Rotation Charter)
(Latest | Earliest) View (newer 50 | older 50) (20 | 50 | 100 | 250 | 500)
