Programming Languages and Systems

DOI10.1007/11693024MaRDI QIDQ5899009zbMATH OpenOpenAlexFDO

Authors Amal Ahmed

Publication date 2 May 2007

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/11693024

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Logic in computer science (03B70) Functional programming and lambda calculus (68N18)

Recommendations

• Syntactic logical relations for polymorphic and recursive types
• Transfinite step-indexing: decoupling concrete and logical steps
• Relational Reasoning for Recursive Types and References
• Step-indexed logical relations for probability
• scientific article; zbMATH DE number 1342222

Cited in

(35)

• Temporal refinements for guarded recursive types
• On the versatility of open logical relations. Continuity, automatic differentiation, and a containment theorem
• Translation certification for smart contracts
• A type-directed, dictionary-passing translation of method overloading and structural subtyping in Featherweight Generic Go
• Relational Reasoning for Recursive Types and References
• A Step-indexed Semantics of Imperative Objects
• Taming the merge operator
• Step-indexed logical relations for probability
• Program equivalence in an untyped, call-by-value functional language with uncurried functions
• Differential logical relations. II: Increments and derivatives
• Relational cost analysis in a functional-imperative setting
• A Complete, Co-inductive Syntactic Theory of Sequential Control and State
• Polarized subtyping
• A Dictionary-Passing Translation of Featherweight Go
• A relational realizability model for higher-order stateful ADTs
• A higher-order abstract syntax approach to verified transformations on functional programs
• Logical relations for coherence of effect subtyping
• Typing termination in a higher-order concurrent imperative language
• A case study in programming coinductive proofs: Howe's method
• Semantic preservation for a type directed translation scheme of Featherweight Go
• Existential types for relaxed noninterference
• A fibrational tale of operational logical relations: pure, effectful and differential
• Observational program calculi and the correctness of translations
• A verified framework for higher-order uncurrying optimizations
• Selective strictness and parametricity in structural operational semantics, inequationally
• scientific article; zbMATH DE number 7324347 (Why is no real title available?)
• Proving correctness of a compiler using step-indexed logical relations
• Transfinite step-indexing: decoupling concrete and logical steps
• A family of syntactic logical relations for the semantics of Haskell-like languages
• scientific article; zbMATH DE number 7407781 (Why is no real title available?)
• Logical predicates in higher-order mathematical operational semantics
• A Kripke logical relation for effect-based program transformations
• Gradual type theory
• Free theorems and runtime type representations
• Syntactic logical relations for polymorphic and recursive types

This page was built for publication: Programming Languages and Systems

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5899009)