Thumbnail
Access Restriction
Open

Author Barman, Kuntal Das ♦ Bertot, Yves
Source Hyper Articles en Ligne (HAL)
Content type Text
File Format PDF
Language English
Subject Keyword CALCULUS OF CONSTRUCTIONS ♦ SEMANTICS ♦ REFLECTION ♦ FORMAL METHODS ♦ TYPE THEORY ♦ info ♦ Computer Science [cs]/Other [cs.OH]
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.
Educational Use Research
Learning Resource Type Report ♦ Article
Publisher Date 2004-03-01
Publisher Institution INRIA