Normalisation by Evaluation

Channel:
Microsoft Research
Subscribers:
344,000
Published on ● Video Link: https://www.youtube.com/watch?v=wyA1jByI89E


Duration: 49:54
357 views
1

Normalisation by Evaluation is a technique to efficiently compute the normal form of, possibly open, lambda terms with respect to beta reduction and rewrite rules. It works by compiling terms into some functional programming language and reading off a term representation from the evaluated program. It has been implemented in the theorem prover Isabelle, and a detailed model has been formally verified. The talk will explain the technique and details of the implementation and verification.



Other Videos By Microsoft Research


2016-09-06Organizing Flickr: Object Mining using Particular Object Retrieval
2016-09-06Augmented Social Cogniton [1/12]
2016-09-06Automatically Finding Patches Using Genetic Programming
2016-09-06Transforming Software Powerhouse to Knowledge Systems Powerhouse
2016-09-06Your Money or Your Life: Nine Steps to Transforming Your Relationship with Money
2016-09-06Scheduling and Synchronization for Multicores
2016-09-06Developing Game-Themed Applications With XNA Game Studio: Session 2
2016-09-06Making Large Legacy Software Run Twice as Fast on a Quad-Core with Just 1 Month of Programmer Effort
2016-09-06(4,4)-split Jacobians of curves of genus 2
2016-09-06Advances in the CM method for elliptic curves
2016-09-06Normalisation by Evaluation
2016-09-06Utilising the Ubiquity of the Cell Phone to Record Physiological Activities
2016-09-06Distributed Storage Systems Made Easy
2016-09-06Software Model Checking for Confidentiality
2016-09-06Out of Our Heads: Why You Are Not Your Brain and Other Lessons from the Biology of Consciousness
2016-09-06Bill Gates, Warren Buffett and Other Great Minds Show how Creative Capitalism Can Save the World
2016-09-06Bayesian infinite matrix factorization
2016-09-06Securing the Web Platform
2016-09-06Volumetric Light Transport for Vision and Graphics
2016-09-06Automatic Workload Evaluation (AWE): Predicting Web 2.0 Workload Behavior
2016-09-06Using Wireless Sensor Data to Enable Intelligent Cooling Control in Data Centers - Case Studies


Tags:
microsoft research