Skip to Main content Skip to Navigation
New interface

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 :
Complete list of metadata

Cited literature [1 references]  Display  Hide  Download
Contributor : Rapport De Recherche Inria Connect in order to contact the contributor
Submitted on : Tuesday, May 23, 2006 - 5:34:25 PM
Last modification on : Friday, February 4, 2022 - 3:16:14 AM
Long-term archiving on: : Sunday, April 4, 2010 - 10:15:12 PM


  • HAL Id : inria-00071449, version 1



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



Record views


Files downloads