NDLI: From dynamic binding to state via modal possibility

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

Automatic verification of cryptographic protocols: a logic programming approach

Towards a formal notion of trust

A functional correspondence between evaluators and abstract machines

Conditional narrowing without conditions

Finding all minimal unsatisfiable subsets

On translating geometric solids to functional expressions

ViMer: a visual debugger for mercury

Rank 2 intersection types for modules

Extending arbitrary solvers with constraint handling rules

Statically assuring secrecy for dynamic concurrent processes

Formally deriving an STG machine

Refining weakly outermost-needed rewriting and narrowing

Simplification and termination of strategies in rule-based languages

On the rewriting and efficient computation of bound disjunctive datalog queries

Term rewriting with variable binding: an initial algebra approach

Compilation of extended recursion in call-by-value functional languages

From datalog rules to efficient programs with time and space guarantees

A framework for typed HOAS and semantics

Explicit substitutions in the reduction of lambda terms

From dynamic binding to state via modal possibility

Integrating finite domain constraints and CLP with sets

Practical aspects of declarative debugging in Haskell 98

Generativity and dynamic opacity for abstract types

A demand-driven narrowing calculus with overlapping definitional trees

Foundational proof checkers with small witnesses

Efficient fixpoint computation in linear tabling

From dynamic binding to state via modal possibility

Content Provider	ACM Digital Library
Author	Nanevski, Aleksandar
Abstract	In this paper we propose a typed, purely functional calculus for state (with second-class locations) in which types reflect the dichotomy between reading from and writing into the global store. This is in contrast to the usual formulation of state via monads, where the primitives for reading and writing introduce the same monadic type constructor. We hope to argue that making this distinction is useful, simple, and has strong logical foundations.Our type system is based on the proof-term calculus for constructive modal logic S4, which has two modal type operators: ␣ for necessity and ◊ for possibility. We extend this calculus with the notion of names (which stand for locations) and generalize to indexed families of modal operators (indexed by sets of names). Then, the modal type ␣CA classifies computations of type A which read from store locations listed in the set C. The dual type ␣CA classifies computations which first write into the locations from \$C\$ and than use the changed store to obtain a value of type A.There are several benefits to this development. First, the necessitation fragment of the language is interesting in its own: it formulates a calculus of dynamic binding. Second, the possibility operator ◊ is a monad, thus forcing the single-threading of memory writes, but not of memory reads (as these are associated with ␣). Finally, the different status of reads and writes gives rise to a natural way of expressing the allocation of uninitialized memory while also providing guarantees that only initialized locations are dereferenced.
Starting Page	207
Ending Page	218
Page Count	12
File Format	PDF
ISBN	1581137052
DOI	10.1145/888251.888271
Language	English
Publisher	Association for Computing Machinery (ACM)
Publisher Date	2003-08-27
Publisher Place	New York
Access Restriction	Subscribed
Subject Keyword	Dynamic binding State Modal lambda-calculus Effect systems
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

From dynamic binding to state via modal possibility (2003)

A Meta Lambda Calculus with Cross-Level Computation

Pure type systems with corecursion on streams: from finite to infinitary normalisation

Extending the lambda-calculus with unbind and rebind

A symmetric modal lambda calculus for distributed computing (2004).

A symmetric modal lambda calculus for distributed computing (2005).

From a concurrent lambda-calculus to the pi-calculus.

Dynamic rebinding for marshalling and update, with destruct-time ?

A Modal Lambda Calculus with Iteration and Case Constructs (1997)

From dynamic binding to state via modal possibility

Similar Documents

From dynamic binding to state via modal possibility (2003)

A Meta Lambda Calculus with Cross-Level Computation

Pure type systems with corecursion on streams: from finite to infinitary normalisation

Extending the lambda-calculus with unbind and rebind

A symmetric modal lambda calculus for distributed computing (2004).

A symmetric modal lambda calculus for distributed computing (2005).

From a concurrent lambda-calculus to the pi-calculus.

Dynamic rebinding for marshalling and update, with destruct-time ?

A Modal Lambda Calculus with Iteration and Case Constructs (1997)

From dynamic binding to state via modal possibility