Optimizing higher-order pattern unification

By Brigitte Pientka and Frank Pfenning, from CADE 2003, available from Frank Pfenning’s website:

We present an abstract view of existential variables in a dependently typed lambda-calculus based on modal type theory. This allows us to justify optimizations to pattern unification such as linearization, which eliminates many unnecessary occurs-checks. The presented modal framework explains a number of features of the current implementation of higher-order unification in Twelf and provides insight into several optimizations. Experimental results demonstrate significant performance improvement in many example applications of Twelf, including those in the area of proof-carrying code.

1 Response to “Optimizing higher-order pattern unification”


  1. 1 free live sex cam March 20, 2014 at 10:20 am

    Terrific works of art! That’s the types of facts that should be distributed around the web. Pity about the search for engines for now not necessarily placing this post increased! Occur more than plus pay a visit to this site. Thanks a lot Equates to)


Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s





%d bloggers like this: