ICFP 2003 - PDF Preprint Papers

ICFP 2003 International Conference on Functional Programming

Teaser Browsing | Click Here

Title Browsing | Click Here

Wall of Fame | Most Viewed ICFP-2003 Paper

click to vote

ICFP
2003
ACM

167views Programming Languages» more ICFP 2003»

Mechanising Hankin and Barendregt using the Gordon-Melham axioms

14 years 4 months ago

Download users.rsise.anu.edu.au

I describe the mechanisation in HOL of some basic -calculus theory, using the axioms proposed by Gordon and Melham [4]. Using these as a foundation, I mechanised the proofs from C...

Michael Norrish

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	167	Mechanising Hankin and Barendregt using the Gordon-Melham axioms	claim
2	162	Compiler implementation in a formal logical framework	claim
3	153	MLF: raising ML to the power of system F	claim
4	136	A static type system for JVM access control	claim
5	129	Dependency-style generic Haskell	claim
6	125	Discriminative sum types locate the source of type errors	claim
7	124	Functional automatic differentiation with dirac impulses	claim
8	123	An effective theory of type refinements	claim
9	120	CDuce: an XML-centric general-purpose language	claim
10	120	Boxes go bananas: encoding higher-order abstract syntax with parametric polymorphism	claim
11	119	FreshML: programming with binders made simple	claim
12	119	A formalization of an Ordered Logical Framework in Hybrid with applications to continuation machines	claim
13	118	Verifying CPS transformations in Isabelle/HOL	claim
14	112	A modal foundation for meta-variables	claim
15	110	Dynamic rebinding for marshalling and update, with destruct-time?	claim
16	109	Iterative-free program analysis	claim
17	108	Software is discrete mathematics	claim
18	108	A theory of aspects	claim
19	107	A sound and complete axiomatization of delimited continuations	claim
20	102	Reasoning on an imperative object-based calculus in Higher Order Abstract Syntax	claim
21	100	An extension of HM(X) with bounded existential and universal data-types	claim
22	93	Optimistic evaluation: an adaptive evaluation strategy for non-strict programs	claim
23	93	Call-by-value is dual to call-by-name	claim
24	93	Explicit substitutions and higher-order syntax	claim
25	91	Scripting the type inference process	claim
26	91	Meta-programming through typeful code representation	claim
27	90	Disjunctive normal forms and local exceptions	claim
28	88	Global abstraction-safe marshalling with hash types	claim
29	87	A user-centred approach to functions in Excel	claim
30	85	Polish parsers, step by step	claim
31	85	Reasoning about recursive procedures with parameters	claim
32	76	Representing reductions of NP-complete problems in logical frameworks: a case study	claim

Sciweavers

Explore & Download

Productivity Tools

Document Tools

Image Tools

Sciweavers