Chapter 5 give us more interesting example of using tactics.
The eapply can leaving the unmatched term to be fixed by future rules matching.
标签
favor site
博文
博客归档
-
▼
2008
(84)
-
▼
十月
(77)
- ICSE 08:ReBA: Refactoring-aware Binary Adaptation ...
- Incremental State-Space Exploration for Programs w...
- Answering Conceptual Queries with Ferret
- Bidirectionalization for Free
- A Cost Semantics for Self-Adjusting Computation
- Local Rely-Guarantee Reasoning
- Static Contract Checking for Haskell
- State-Dependent Representation Independence
- a good survey of Mixed Transition Systems
- usb device not recognized on CentOS 5.2 over dell ...
- porting/using the state of the art applications in...
- can type system be dynamic?
- primitive recursion and general recursion
- Handbook of Automated Reasoning
- type system list
- Hindley–Milner type inference algorithm
- pointer type
- yet another learn on dependent type
- Some issue that may interference with my idea on r...
- Curry-Howard correspondence
- Programming in Martin-Löf's Type Theory
- VMCAI 09 : Reducing Behavioural to Structural Prop...
- VMCAI 09: Shape-value Abstraction for Verifying Li...
- Inital consideration for regular data structure en...
- VMCAI 09: LTL Generalized Model Checking Revisited
- LICS 08 paper list and their link
- Design OS with full FL or Fl sematics
- ICFP 08 : NixOS: A Purely Functional Linux Distrib...
- ICFP 2008 paper's link
- 我给新来博士生的入门资料列表
- Essentials of Programming Languages itpub
- Richard Bornat (Middlesex page)
- VMCAI 09 accepted paper and their link
- Another list of ASPDAC accepted paper
- ASPDAC 09 accepted paper and their link
- POPL 09 accepted papers and their link
- Upcoming conf
- from data to structrue
- Typed assembly language
- A very light weight VM at application level and ca...
- protect OS itself from affected
- Guide to the history of web application framwork
- design special hardware to boost functional language
- Using library without reading documentation??
- OSDI 08 : Hardware Enforcement of Application Secu...
- OSDI 08 : Difference Engine: Harnessing Memory Red...
- OSDI 08: DryadLINQ: A System for General-Purpose D...
- OSDI 08: CuriOS: Improving Reliability through Ope...
- OSDI'08 : Corey: an operating system for many cores
- U Rank:collaborating searching
- OSDI 08 : Improving MapReduce Performance in Heter...
- a glue to merge the gap between two agent automaticly
- Dawson Engler is back
- powerful e* tactic
- web related topic
- virtual machine as identification function
- reasoning across language
- dependent product
- what is the defference between dependent product a...
- compositions
- varias tatics of propositional logic
- guessing the relation of proof and model theory
- Johan.Sebastian.-.[Ultimate.Bach.CD1].专辑.(FLAC)
- relation of the 3 proof caculis in proof theory
- balance of axiom and inference rules
- a large collection of math proof
- proof theory and model theory
- Curry-Howard correspondence
- strong normalization
- globla environment和local context
- coq art pdf file
- varias logic system
- Per Martin-Löf
- FP和LP的关系
- 正式开始coq art
- coq art djvu file
- I am still hacking CIL and its CFG package, but it...
-
▼
十月
(77)
没有评论:
发表评论