Another Type System for In-Place Update

No abstract is available for this paper.

• Publication year

  2002

• Venue

  European Symposium on Programming

• Publication date

  2002-04-08

• Fields of study

  Computer Science

• Identifiers
  DOI 10.1007/3-540-45927-8_4
• External record

  Open on Semantic Scholar

• Source metadata

  Semantic Scholar

• No claims are published for this paper.

• No concepts are published for this paper.

• Heap-Bounded Assembly Language

  2004cited by this paper
• The strength of non-size increasing computation

  2002cited by this paper
• BI as an assertion language for mutable data structures

  2001cited by this paper
• Alias Types

  2000cited by this paper
• Shape Analysis

  2000cited by this paper
• A Type System for Bounded Space and Functional In-Place Update

  2000influential reference
• Simple Usage Polymorphism

  2000cited by this paper
• Typed memory management in a calculus of capabilities

  1999cited by this paper
• Linear types and non-size-increasing polynomial time computation

  1999cited by this paper
• The Logic of Bunched Implications

  1999cited by this paper
• Quasi-linear types

  1999cited by this paper
• Syntactic control of interference revisited

  1999cited by this paper
• Intuitionistic reasoning about shared mutable data structure

  1999cited by this paper
• Set constraints for destructive array update optimization

  1998cited by this paper
• Region-based Memory Management

  1997cited by this paper
• Imperative Lambda Calculus Revisited

  1997cited by this paper
• Uniqueness typing for functional languages with graph rewriting semantics

  1996cited by this paper
• A Uniform Treatment of Order of Evalaution and Aggregate Update

  1993cited by this paper
• Observers for Linear Types

  1992cited by this paper
• Linear Types can Change the World!

  1990cited by this paper
• Syntactic control of interference

  1978cited by this paper

• Weak-Linear Types

  2024cites this paper
• Weak-linearity, globality and in-place update

  2024cites this paper
• FP²: Fully in-Place Functional Programming

  2023cites this paper
• Morpheus: Automated Safety Verification of Data-dependent Parser Combinator Programs

  2023cites this paper
• A Framework for the Automated Verification of Algebraic Effects and Handlers (extended version)

  2023cites this paper
• A High-Level Separation Logic for Heap Space under Garbage Collection

  2023influential citation
• Two Parametricities Versus Three Universal Types

  2022cites this paper
• A separation logic for heap space under garbage collection

  2022cites this paper
• Logical Relations for Partial Features and Automatic Differentiation Correctness

  2022cites this paper
• A Review of consensus protocols in permissioned blockchains

  2021cites this paper
• SteelCore: an extensible concurrent separation logic for effectful dependently typed programs

  2020cites this paper
• The Correctness of a Code Generator for a Functional Language

  2020cites this paper
• Efficient Verification of Optimized Code: Correct High-speed Curve25519

  2020cites this paper
• Optimal stateless model checking under the release-acquire semantics

  2018cites this paper
• Contextual Modal Type Theory with Polymorphic Contexts

  2018cites this paper
• Higher-order contracts for JavaScript

  2018cites this paper
• A survey of real‐time capabilities in functional languages and compilers

  2018cites this paper
• A methodology for trustworthy file systems

  2016cites this paper
• Quantitative bounds on the security-critical resource consumption of JavaScript apps

  2016cites this paper
• Concurrent Data Structures Linked in Time

  2016cites this paper
• Approaches for Software Verification of An Emergency Recovery System for Micro Air Vehicles

  2014cites this paper
• A FIREWALL MODEL OF FILE SYSTEM SECURITY

  2014cites this paper
• A Survey of Concepts Location Enhancement for Program Comprehension and Maintenance

  2014cites this paper
• Safety properties and memory bound analysis in a functional language without a garbage collector

  2011influential citation
• Improving Strategies via SMT Solving

  2011cites this paper
• Automated amortised analysis

  2010cites this paper
• Certified Absence of Dangling Pointers in a Language with Explicit Deallocation

  2010cites this paper
• Size-Change Termination and Transition Invariants

  2010cites this paper
• Bonnes démonstrations en déduction modulo

  2009cites this paper
• An Inference Algorithm for Guaranteeing Safe Destruction

  2009cites this paper
• Implementing logical synchrony in integrated modular avionics

  2009cites this paper
• A Proof-Carrying-Code Infrastructure for Resources

  2009cites this paper
• A type system for safe memory management and its proof of correctness

  2008cites this paper
• Abstraction-level functional programming

  2008cites this paper
• AHA: Amortized Heap Space Usage Analysis. Project Paper

  2007cites this paper
• L ^3 : A Linear Language with Locations

  2007cites this paper
• L 3 : A Linear Language with Locations

  2007cites this paper
• AHA: Amortized Heap Space Usage Analysis

  2007cites this paper
• The Embounded Project

  2006cites this paper
• Substructural Simple Type Theories for Separation and In-place Update

  2006cites this paper
• Estimating the Cost of Native Method Calls for Resource-bounded Functional Programming Languages

  2006cites this paper
• The Parma Polyhedra Library: Toward a complete set of numerical abstractions for the analysis and verification of hardware and software systems

  2006cites this paper
• Verified proof carrying code

  2006cites this paper
• Verified proof carrying code

  2006cites this paper
• Types with semantics: soundness proof assistant

  2005influential citation
• Static insertion of safe and effective memory reuse commands into ML-like programs

  2005cites this paper
• Amortized Heap-Space Analysis for First-Order Functional Programs

  2005cites this paper
• AHA A mortized H eap Space Usage A nalysis

  2005cites this paper
• Memory Consumption Analysis of Java Smart Cards

  2005cites this paper
• Automatic Certification of Heap Consumption

  2005influential citation
• Precise analysis of memory consumption using program logics

  2005cites this paper
• A step-indexed model of substructural state

  2005cites this paper
• Sixth Framework Programme Fp6 Priority 2 Information Society Technologies Specific Targeted Research or Innovation Project Annex I – " Description of Work "

  2004cites this paper
• Towards certificate generation for linear heap consumption

  2004cites this paper
• Lfd_infer: an Implementation of a Static Inference on Heap Space Usage

  2004cites this paper
• Case for Support Computing with arbitrary precision curves Dr .

  2004cites this paper
• Experiments on the effectiveness of an automatic insertion of memory reuses into ML-like programs

  2004influential citation
• A Program Logic for Resource Verification

  2004cites this paper
• Mobile Resource Guarantees for Smart Devices

  2004cites this paper
• Advanced Topics In Types And Programming Languages

  2004cites this paper
• Heap-Bounded Assembly Language

  2004cites this paper
• Model-Theoretic Methods in Combined Constraint Satisfiability

  2004cites this paper
• Camelot and Grail: resource-aware functional programming for the JVM

  2003cites this paper
• A Linearly Typed Assembly Language

  2003influential citation
• Is it time for real-time functional programming?

  2003cites this paper
• Inserting Safe Memory Re-use Commands into ML-like Programs

  2003cites this paper
• Functional In-Place Update with Layered Datatype Sharing

  2003cites this paper
• Correctness Proof on an Algorithm to Insert Memory Reuse Commands into ML-like

  2003influential citation
• Static prediction of heap space usage for first-order functional programs

  2003cites this paper
• Grail: a functional form for imperative mobile code

  2003influential citation
• LFPL with Types for Deep Sharing

  2002cites this paper
• Typing with Conditions and Guarantees for Functional In-place Update

  2002influential citation
• Extending resource-bounded functional programming languages with mutable state and concurrency

  2001cites this paper
• Type Classes and Constraint Handling Rules

  2000cites this paper
• Certification of Resource Consumption : from Types to Logic ( Programming )

  year unknowncites this paper
• School of Informatics , University of Edinburgh Laboratory for Foundations of Computer Science Typing with Conditions and Guarantees in LFPL by Michal Konecny Informatics Research Report

  year unknowninfluential citation
• Under Consideration for Publication in J. Functional Programming a Type System with Usage Aspects

  year unknowncites this paper