A syntactic approach to type soundness
From MaRDI portal
Publication:1341754
DOI10.1006/inco.1994.1093zbMath0938.68559OpenAlexW1980939032WikidataQ55952333 ScholiaQ55952333MaRDI QIDQ1341754
Matthias Felleisen, Andrew K. Wright
Publication date: 21 June 2000
Published in: Information and Computation (Search for Journal in Brave)
Full work available at URL: https://semanticscholar.org/paper/c19c45531a5f6c114e9da1dbfea8aedc31c31e0d
Related Items
Modular structural operational semantics, A simplified account of polymorphic references, Soundness Conditions for Big-Step Semantics, A Functional Abstraction of Typed Invocation Contexts, Certifying low-level programs with hardware interrupts and preemptive threads, Type inference for record concatenation and subtyping, From Outermost Reduction Semantics to Abstract Machine, The Negligible and Yet Subtle Cost of Pattern Matching, Typed Relational Conversion, Eliom: A Core ML Language for Tierless Web Programming, A note on ``A simplified account of polymorphic references, Compilation of extended recursion in call-by-value functional languages, A Rewriting Logic Approach to Type Inference, Semantic subtyping with an SMT solver, Unnamed Item, A Delta for Hybrid Type Checking, A core calculus for correlation in orchestration languages, Formal verification of concurrent programs with Read-write locks, Dynamic overloading with copy semantics in object-oriented languages: a formal account, Mechanising a type-safe model of multithreaded Java with a verified compiler, simpA: an agent-oriented approach for programming concurrent applications on top of Java, From Rewriting Logic, to Programming Language Semantics, to Program Verification, A functional approach to generic programming using adaptive traversals, An imperative object calculus, The rewriting logic semantics project: a progress report, Implicit typing à la ML for the join-calculus, A graph-based generic type system for object-oriented programs, Lightweight family polymorphism, The expressive power of Structural Operational Semantics with explicit assumptions, From semantics to types: the case of the imperative \(\lambda\)-calculus, Streams of approximations, equivalence of recursive effectful programs, A reduction semantics for direct-style asynchronous observables, Asynchronous correspondences between hybrid trajectory semantics, A linear logical framework, The reflective higher-order calculus: encodability, typability and separation, Effekt: Capability-passing style for type- and effect-safe, extensible effect handlers in Scala, A list-machine benchmark for mechanized metatheory, Gradual type-and-effect systems, A simple library implementation of binary sessions, Unnamed Item, Unnamed Item, Matching MyType to subtyping, Unnamed Item, Context-Free Session Type Inference, Unnamed Item, Contracts made manifest, Polymorphic Contracts, Proving Isolation Properties for Software Transactional Memory, Type-Based Access Control in Data-Centric Systems, From CML to its process algebra, Backwards type analysis of asynchronous method calls, Flag-based big-step semantics, The spirit of ghost code, Syntactic soundness proof of a type-and-capability system with hidden state, Multimodal Separation Logic for Reasoning About Operational Semantics, A type system for counting instances of software components, Weak updates and separation logic, Termination checking with types, An abstract monadic semantics for value recursion, Syntactic Type Soundness for the Region Calculus, A WSDL-based type system for asynchronous WS-BPEL processes, What is the meaning of these constant interruptions?, Delegation by object composition, Typing termination in a higher-order concurrent imperative language, Linear type theory for asynchronous session types, Reconciling method overloading and dynamically typed scripting languages, Unnamed Item, An overview of the K semantic framework, Type inference and strong static type checking for Promela, A Classical Realizability Model for a Semantical Value Restriction, Amalgamating sessions and methods in object-oriented languages with generics, A Context-based Approach to Proving Termination of Evaluation, Typing Safe Deallocation, Abstracting models of strong normalization for classical calculi, A type safe state abstraction for coordination in JAVA-like languages, Mobility control via passports, Coinductive big-step operational semantics, A rewriting logic approach to operational semantics, The Rewriting Logic Semantics Project: A Progress Report, Equational Reasoning About Quantum Protocols, A Type System for Usage of Software Components, Full Abstraction at Package Boundaries of Object-Oriented Languages, Intersection, Universally Quantified, and Reference Types, Revised6 Report on the Algorithmic Language Scheme, Small-step and big-step semantics for call-by-need, Non-disclosure for distributed mobile code, On a monadic semantics for freshness, Dynamic structural operational semantics, Syntactic type soundness results for the region calculus, Modular statically typed multimethods, Structuring Operational Semantics: Simplification and Computation, Prototyping Concurrent Systems with Agents and Artifacts: Framework and Core Calculus, Taming the Merge Operator, A Rewriting Logic Approach to Operational Semantics (Extended Abstract)
