ICFP 2006 - PDF Preprint Papers

ICFP 2006 International Conference on Functional Programming

Teaser Browsing | Click Here

Title Browsing | Click Here

Wall of Fame | Most Viewed ICFP-2006 Paper

click to vote

ICFP
2006
ACM

206views Programming Languages» more ICFP 2006»

Modular development of certified program verifiers with a proof assistant

15 years 12 days ago

Download adam.chlipala.net

I report on an experience using the Coq proof assistant to develop a program verification tool with a machine-checkable proof of full correctness. The verifier is able to prove me...

Adam J. Chlipala

claim paper

Read More »

Disclaimer and Copyright Notice

Sciweavers respects the rights of all copyright holders and in this regard, authors are only allowed to share a link to their preprint paper on their own website. Every contribution is associated with a desciptive image. It is the sole responsibility of the authors to ensure that their posted image is not copyright infringing. This service is compliant with IEEE copyright.

Id	Views	Title	Status

1	206	Modular development of certified program verifiers with a proof assistant	claim
2	198	biXid: a bidirectional transformation language for XML	claim
3	179	Context-parametric polykinded types	claim
4	175	Access control in a core calculus of dependency	claim
5	158	Polymorphism and separation in hoare type theory	claim
6	150	Design patterns as higher-order datatype-generic programs	claim
7	147	Boxy types: inference for higher-rank types and impredicativity	claim
8	139	Algebraic fusion of functions with an accumulating parameter and its improvement	claim
9	137	Delimited dynamic binding	claim
10	135	Programming monads operationally with Unimo	claim
11	131	Static analysis for syntax objects	claim
12	130	A pattern for almost compositional functions	claim
13	124	Stabilizers: a modular checkpointing abstraction for concurrent functional programs	claim
14	123	Simple unification-based type inference for GADTs	claim
15	122	An object-oriented approach to datatype-generic programming	claim
16	121	Modular generic programming with extensible superclasses	claim
17	120	Extensible programming with first-class cases	claim
18	117	Good advice for type-directed programming aspect-oriented programming and extensible generic functions	claim
19	117	Type-theoretic design patterns	claim
20	116	Towards an automatic complexity analysis for generic programs	claim
21	114	Modelling deterministic concurrent I/O	claim
22	114	The missing link: dynamic components for ML	claim
23	110	Abstraction preservation and subtyping in distributed languages	claim
24	110	From structures and functors to modules and units	claim
25	110	Generating generic functions	claim
26	103	The development of Chez Scheme	claim
27	100	Static typing for a faulty lambda calculus	claim
28	99	Transactional events	claim
29	97	Recursive modules for programming	claim
30	95	A technique for generic iteration and its optimization	claim
31	92	Mechanized meta-reasoning using a hybrid HOAS/de bruijn representation and reflection	claim
32	77	OCaml + XDuce	claim

Sciweavers

Explore & Download

Productivity Tools

Document Tools

Image Tools

Sciweavers