Sign in
Author

Conference

Journal

Organization

Year

DOI
Look for results that meet for the following criteria:
since
equal to
before
between
and
Search in all fields of study
Limit my searches in the following fields of study
Agriculture Science
Arts & Humanities
Biology
Chemistry
Computer Science
Economics & Business
Engineering
Environmental Sciences
Geosciences
Material Science
Mathematics
Medicine
Physics
Social Science
Multidisciplinary
Keywords
(3)
Functional Language
Programming Language
Type Theory
Related Publications
(2)
Certification of a Type Inference Tool for ML: DamasMilner within Coq
From Semantics to Rules: A Machine Assisted Analysis
Subscribe
Academic
Publications
A Machineassisted Proof that Well Typed Expressions Cannot Go Wrong
A Machineassisted Proof that Well Typed Expressions Cannot Go Wrong,Ana Bove
Edit
A Machineassisted Proof that Well Typed Expressions Cannot Go Wrong
(
Citations: 4
)
BibTex

RIS

RefWorks
Download
Ana Bove
This paper deals with the application of constructive
type theory
to the theory of programming languages. The main aim of this work is to investigate constructive formalisations of the mathematics of programs. Here, we consider a small typed
functional language
and prove some properties about it, arriving at the property that establishes that well typed expressions cannot go wrong. First, we give the definitions and proofs in an informal style, and then we present and explain the formalisation...
Published in 1998.
Cumulative
Annual
Citation Context
(3)
...Lastly, in [
3
], A. Bove uses a reduction semantics but in the restricted monomorphic case (ALF)...
Catherine Dubois
.
Proving ML Type Soundness Within Coq
...Many authors have proved theorems about simply and dependently typed lambda calculi inside type theory proof assistants, for example, Coquand [6], Bove [
4
] (in ALF), McKinna and Pollack [15], Altenkirch [1] (in LEGO), and B. Barras [3], Huet [12], Sa¨bi [19] (in Coq)...
Qiao Haiyan
.
Formalising FormulasasTypesasObjects
...[5, 4,
3
, 12, 9, 15, 11, 13]), no publication mentions the computerverifled formalization and proof of type soundness for a fragment of ML mixing imperative and functional primitives...
Olivier Boite
,
et al.
Proving Type Soundness of a Simply Typed MLLike Language with Referen...
References
(9)
A Theory of Type Polymorphism in Programming
(
Citations: 1408
)
Robin Milner
Journal:
Journal of Computer and System Sciences  JCSS
, vol. 17, no. 3, pp. 348375, 1978
Logic Programming in the LF Logical Framework
(
Citations: 201
)
Frank Pfenning
Published in 1991.
Natural Semantics and Some of Its MetaTheory in Elf
(
Citations: 50
)
Spiro Michaylov
,
Frank Pfenning
Conference:
Extensions of Logic Programming  ELP
, pp. 299344, 1991
The alf proof editor and its proof engine
(
Citations: 75
)
Lena Magnusson
,
Bengt Nordstrsm
Conference:
Types for Proofs and Programs
, 1994
Type Theory and Programming
(
Citations: 25
)
Bengt Nordstrom
,
Bjorn Von Sydow
,
Jan M. Smith
,
Thierry Coquand
Published in 1994.
Sort by:
Citations
(4)
Proving ML Type Soundness Within Coq
(
Citations: 12
)
Catherine Dubois
Conference:
Theorem Proving in Higher Order Logics  TPHOLs
, pp. 126144, 2000
Formalising FormulasasTypesasObjects
(
Citations: 3
)
Qiao Haiyan
Conference:
Types for Proofs and Programs
, pp. 174193, 1999
Proving Type Soundness of a Simply Typed MLLike Language with References
(
Citations: 3
)
Olivier Boite
,
Catherine Dubois
Conservatoire National des Arts et Metiers
Olivier BOITE