Proof by reflection in semantics

Kuntal das Barman 1 Yves Bertot
1 LEMME - Software and mathematics
CRISAM - Inria Sophia Antipolis - Méditerranée
Abstract : Conventional approach to describe the semantics of programming language usually rely on relations, in particular inductive relations. Simulating program execution then relies on proof search tools. We describe a functional approach to automate proofs about programming language semantics. Reflection is used to take facts from the context into account. The main contribution of this work is that we developed a systematic approach to describe and manipulate unknown expressions in the symbolic computation of programs for formal proof development. The tool we obtain is faster and more powerful than the conventional proof tools.
Document type :
Reports
Complete list of metadatas

Cited literature [1 references]  Display  Hide  Download

https://hal.inria.fr/inria-00071449
Contributor : Rapport de Recherche Inria <>
Submitted on : Tuesday, May 23, 2006 - 5:34:25 PM
Last modification on : Monday, September 3, 2018 - 10:56:02 AM
Long-term archiving on: Sunday, April 4, 2010 - 10:15:12 PM

Identifiers

  • HAL Id : inria-00071449, version 1

Collections

Citation

Kuntal das Barman, Yves Bertot. Proof by reflection in semantics. RR-5134, INRIA. 2004. ⟨inria-00071449⟩

Share

Metrics

Record views

131

Files downloads

341