Sciweavers

Share
warning: Creating default object from empty value in /var/www/modules/taxonomy/taxonomy.module on line 1416.
SCP
2011
255views Communications» more  SCP 2011»
11 years 16 days ago
Map fusion for nested datatypes in intensional type theory
A definitional extension LNGMIt of the Calculus of Inductive Constructions (CIC), that underlies the proof assistant Coq, is presented that allows also to program with nested dat...
Ralph Matthes
JSC
2002
84views more  JSC 2002»
11 years 5 months ago
A Constructive Algebraic Hierarchy in Coq
We describe a framework of algebraic structures in the proof assistant Coq. We have developed this framework as part of the FTA project in Nijmegen, in which a constructive proof ...
Herman Geuvers, Randy Pollack, Freek Wiedijk, Jan ...
JAR
2002
77views more  JAR 2002»
11 years 5 months ago
Proof Reflection in Coq
We formalise natural deduction for first-order logic in the proof assistant Coq, using De Bruijn indices for variable binding. The main judgement we model is of the form d [:] , ...
Dimitri Hendriks
JAR
2007
123views more  JAR 2007»
11 years 5 months ago
Reasoning about Object-based Calculi in (Co)Inductive Type Theory and the Theory of Contexts
Abstract. We illustrate a methodology for formalizing and reasoning about Abadi and Cardelli’s object-based calculi, in (co)inductive type theory, such as the Calculus of (Co)Ind...
Alberto Ciaffaglione, Luigi Liquori, Marino Micula...
CORR
2007
Springer
125views Education» more  CORR 2007»
11 years 5 months ago
Common knowledge logic in a higher order proof assistant?
This paper presents experiments on common knowledge logic, conducted with the help of the proof assistant Coq. The main feature of common knowledge logic is the eponymous modality...
Pierre Lescanne
ENTCS
2006
153views more  ENTCS 2006»
11 years 5 months ago
Automatic Complexity Analysis for Programs Extracted from Coq Proof
We describe an automatic complexity analysis mechanism for programs extracted from proofs carried out with the proof assistant Coq. By extraction, we mean the automatic generation...
Jean-Pierre Jouannaud, Weiwen Xu
CORR
2006
Springer
99views Education» more  CORR 2006»
11 years 5 months ago
Inductive types in the Calculus of Algebraic Constructions
In a previous work, we proved that almost all of the Calculus of Inductive Constructions (CIC), the basis of the proof assistant Coq, can be seen as a Calculus of Algebraic Constru...
Frédéric Blanqui
CORR
2006
Springer
110views Education» more  CORR 2006»
11 years 5 months ago
Definitions by Rewriting in the Calculus of Constructions
Abstract : The main novelty of this paper is to consider an extension of the Calculus of Constructions where predicates can be defined with a general form of rewrite rules. We prov...
Frédéric Blanqui
ENTCS
2008
136views more  ENTCS 2008»
11 years 5 months ago
Multimodal Separation Logic for Reasoning About Operational Semantics
We show how to reason, in the proof assistant Coq, about realistic programming languages using a combination of separation logic and heterogeneous multimodal logic. A heterogeneou...
Robert Dockins, Andrew W. Appel, Aquinas Hobor
CORR
2008
Springer
102views Education» more  CORR 2008»
11 years 5 months ago
(Mechanical) Reasoning on Infinite Extensive Games
In order to better understand reasoning involved in analyzing infinite games in extensive form, we performed the experiments in proof assistant Coq that are reported here.
Pierre Lescanne
books