Reasoning about Computations Using Two Levels of Logic

Dale Miller

Description

Niveau: Supérieur
Reasoning about Computations Using Two-Levels of Logic Dale Miller INRIA-Saclay & LIX/Ecole Polytechnique Palaiseau, France APLAS 2010, 1 December 2010, Shanghai

• sometimes capture


• computations using


• dynamic semantics


• must judgments


• related work


• deep results


• effort spans


• finite state


• semantics

Sujets

• École polytechnique
• Programming language
• Finite-state machine
• Semantics

Informations

• Publié par: chaeh
• Nombre de lectures: 9
• Langue: English

Extrait

Reasoning about Computations Using Two-Levels of Logic

Dale Miller

´ INRIA-Saclay & LIX/Ecole Polytechnique Palaiseau, France

APLAS 2010, 1 December 2010, Shanghai

Overview of high-level goals

I Design e.g.,a logic for reasoning about computation: capture I inductive and co-inductive reasoning, I may and must judgments, and I binding and substitution. I Reasondirectly on logic specifications of computation. I Formalizelogic as proof theory in the traditionthe reasoning of Gentzen and Girard. I Implementthe proof theory and apply to examples.

This research effort spans the years 1997 to 2010 and has involved about 6 researchers.

Outline

A logic for specifications

The open and closed world assumptions

Generic quantification

The Abella prover

Related work: nominal logic and POPLMark

Outline

A logic for specifications

The open and closed world assumptions

Generic quantification

The Abella prover

Related work: nominal logic and POPLMark