Proof by reflection in semantics

Kuntal das Barman (1) , Yves Bertot

1 LEMME - Software and mathematics

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.

Mots clés: FORMAL METHODS; TYPE THEORY; CALCULUS OF CONSTRUCTIONS; SEMANTICS; REFLECTION

Domaines: Autre [cs.OH]

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