NDLI: Proof-oriented and applicative valuations in definitions of algorithms

Please wait, while we are loading the content...

Function level programs as mathematical objects

FP with data abstraction and strong typing

Applicative style programming, program transformation, and list operators

A simple optimizer for FP-like languages

Transformations of FP program schemes

Programming with concrete data structures and sequential algorithms

Operators and algebraic structures

ALICE a multi-processor reduction machine for the parallel evaluation CF applicative languages

Resource management in dataflow

The semantic elegance of applicative languages

Copying operands versus copying results: A solution to the problem of large operands in FFP'S

Optimal associative searching on a cellular computer

Communication along shortest paths in a tree machine

Implanting FFP trees in binary trees: An architectural proposal

Applications of feedback in functional programming

Applicative caching: Programmer control of object sharing and lifetime in. distributed implementations of applicative languages

Programming in Constructive Set Theory: Some examples

Proof-oriented and applicative valuations in definitions of algorithms

Parallel interpretation of logic programs

A relational language for parallel programming

If-then-else as a concurrency inhibitor in eager beaver evaluation of recursive programs

Executing functional programs on a virtual tree of processors

A practical functional programming system for databases

A data-flow language for specifying business data processing applications

Introduction to relational programming

Specification of data structures for FP programs

Proof-oriented and applicative valuations in definitions of algorithms

Content Provider	ACM Digital Library
Author	Sintzoff, Michel
Abstract	Our aim is to investigate means for expressing programs and their design, in such a way that the logical consistency of each expression be ensured constructively, and that the structure of the expressions be general and elegant. It is more and more apparent that the latter requirement is better ensured by functional constructs, viz. by pure expressions; indeed much attention is nowadays being paid to this aspect. But the treatment of the logic of the expressions is much less studied; as a rule, properties are proved by using an algebra of expressions [1,2] or by explicitly applying a powerful induction rule such as Scott's. The approach we propose is as follows, roughly speaking. To each expression we shall ascribe a pair of logical expressions, viz. the precondition and the postcondition. Then, in principle, the compatibility of an expression with a proposed input-ouput assertion is verified in three steps: to ascribe correct input-output assertions to the basic component expressions, to 'evaluate' the expression, and finally to check the resulting input-output assertion validates the proposed one. Thus neither preconditions nor postconditions should be privileged: both together are parameters and results of the valuations. 'Backwards', 'forward' are operational concepts we want to abstract from. The paper is organized as follows. First a hypothetical language of expressions is introduced, and the description of the input-output assertions follows. Then, we show how to evaluate expressions in terms of these assertions, also in the recursive case. A couple of examples and a case study illustrate how to prove properties in that framework. Finally, open problems, related works, and possible plans are discussed. Altogether, the paper gives a preliminary account of the proposals rather than a technically complete development.
Starting Page	155
Ending Page	162
Page Count	8
File Format	PDF
ISBN	0897910605
DOI	10.1145/800223.806774
Language	English
Publisher	Association for Computing Machinery (ACM)
Publisher Date	1981-10-18
Publisher Place	New York
Access Restriction	Subscribed
Content Type	Text
Resource Type	Article

Sl.	Authority	Responsibilities	Communication Details
1	Ministry of Education (GoI), Department of Higher Education	Sanctioning Authority	https://www.education.gov.in/ict-initiatives
2	Indian Institute of Technology Kharagpur	Host Institute of the Project: The host institute of the project is responsible for providing infrastructure support and hosting the project	https://www.iitkgp.ac.in
3	National Digital Library of India Office, Indian Institute of Technology Kharagpur	The administrative and infrastructural headquarters of the project	Dr. B. Sutradhar bsutra@ndl.gov.in
4	Project PI / Joint PI	Principal Investigator and Joint Principal Investigators of the project	Dr. B. Sutradhar bsutra@ndl.gov.in Prof. Saswat Chakrabarti will be added soon
5	Website/Portal (Helpdesk)	Queries regarding NDLI and its services	support@ndl.gov.in
6	Contents and Copyright Issues	Queries related to content curation and copyright issues	content@ndl.gov.in
7	National Digital Library of India Club (NDLI Club)	Queries related to NDLI Club formation, support, user awareness program, seminar/symposium, collaboration, social media, promotion, and outreach	clubsupport@ndl.gov.in
8	Digital Preservation Centre (DPC)	Assistance with digitizing and archiving copyright-free printed books	dpc@ndl.gov.in
9	IDR Setup or Support	Queries related to establishment and support of Institutional Digital Repository (IDR) and IDR workshops	idr@ndl.gov.in

On the Proof Theory of Applicative Theories (1996)

Arithmetic algorithms in a proof-oriented set-theoretic language

Applications of applicative proof search

Truth in applicative theories

Truth in applicative theories (2001).

Algorithmic pricing via virtual valuations

The proof-theoretic analysis of the Suslin operator in applicative theories (2002)

What processes know: Definitions and proof methods

On the Proof Theory of Applicative Theories

Proof-oriented and applicative valuations in definitions of algorithms

Similar Documents

On the Proof Theory of Applicative Theories (1996)

Arithmetic algorithms in a proof-oriented set-theoretic language

Applications of applicative proof search

Truth in applicative theories

Truth in applicative theories (2001).

Algorithmic pricing via virtual valuations

The proof-theoretic analysis of the Suslin operator in applicative theories (2002)

What processes know: Definitions and proof methods

On the Proof Theory of Applicative Theories

Proof-oriented and applicative valuations in definitions of algorithms