Step-Indexed Syntactic Logical Relations for Recursive and Quantified Types

No abstract is available for this paper.

• Publication year

  2006

• Venue

  European Symposium on Programming

• Publication date

  2006-03-27

• Fields of study

  Computer Science

• Identifiers
  DOI 10.1007/11693024_6
• External record

  Open on Semantic Scholar

• Source metadata

  Semantic Scholar

• No claims are published for this paper.

• No concepts are published for this paper.

• Syntactic Logical Relations for Polymorphic and Recursive Types

  2007influential reference
• Recursive polymorphic types and parametricity in an operational framework

  2005influential reference
• A bisimulation for type abstraction and recursion

  2005cited by this paper
• Advanced Topics In Types And Programming Languages

  2004cited by this paper
• Semantics of types for mutable state

  2004cited by this paper
• Semantic types: a fresh look at the ideal model for types

  2004cited by this paper
• An Indexed Model of Impredicative Polymorphism and Mutable References

  2003cited by this paper
• Types and programming languages: the next generation

  2003cited by this paper
• An indexed model of recursive types for foundational proof-carrying code

  2001influential reference
• Relational Interpretations of Recursive Types in an Operational Setting

  1999cited by this paper
• Existential Types: Logical Relations and Operational Equivalence

  1998cited by this paper
• Relational Interpretations of Recursive Types in an operational Setting (Summary)

  1997cited by this paper
• Relational Properties of Domains

  1996cited by this paper
• Equivalence in functional languages with effects

  1991cited by this paper
• Theorems for free!

  1989cited by this paper
• An ideal model for recursive polymorphic types

  1984cited by this paper
• Interpretation fonctionelle et elimination des coupures dans l'aritmetique d'ordre superieur

  1972cited by this paper
• Intensional interpretations of functionals of finite type I

  1967cited by this paper

• Machine-Generated, Machine-Checked Proofs for a Verified Compiler (Experience Report)

  2026cites this paper
• Call-by-value and call-by-name: A simple proof of a classic theorem

  2025cites this paper
• A Graded Modal Approach to Relaxed Semantic Declassification

  2025cites this paper
• End-to-end Compositional Verification of Program Safety through Verified and Verifying Compilation

  2025cites this paper
• Affect: An Affine Type and Effect System

  2025cites this paper
• Information Flow Control in Cyclic Process Networks

  2024cites this paper
• Gradually Typed Languages Should Be Vigilant!

  2024cites this paper
• Realistic Realizability: Specifying ABIs You Can Count On

  2024cites this paper
• The Long Way to Deforestation: A Type Inference and Elaboration Technique for Removing Intermediate Data Structures

  2024influential citation
• Bialgebraic Reasoning on Higher-order Program Equivalence

  2024cites this paper
• Probabilistic Programming with Programmable Variational Inference

  2024cites this paper
• Regrading Policies for Flexible Information Flow Control in Session-Typed Concurrency

  2024cites this paper
• Sensitivity by Parametricity

  2024cites this paper
• Denotational Semantics of Gradual Typing using Synthetic Guarded Domain Theory

  2024cites this paper
• Compactness via Pattern Stepping Bisimulation

  2024cites this paper
• Fully Composable and Adequate Verified Compilation with Direct Refinements between Open Modules

  2023cites this paper
• : PURE, EFFECTFUL

  2023cites this paper
• A Fibrational Tale of Operational Logical Relations

  2023cites this paper
• Contextual Linear Types for Differential Privacy

  2023cites this paper
• Step-Indexed Logical Relations for Countable Nondeterminism and Probabilistic Choice

  2023cites this paper
• Parametric Subtyping for Structural Parametric Polymorphism

  2023cites this paper
• Taypsi: Static Enforcement of Privacy Policies for Policy-Agnostic Oblivious Computation

  2023cites this paper
• Gradual Sensitivity Typing

  2023cites this paper
• A Bottom-Up Approach to a Unified Semantic Interface for Verified Compositional Compilation

  2023cites this paper
• Modeling Reachability Types with Logical Relations: Semantic Type Soundness, Termination, Effect Safety, and Equational Theory

  2023cites this paper
• Logical Relations for Session-Typed Concurrency

  2023cites this paper
• A frame stack semantics for sequential Core Erlang

  2023cites this paper
• Semantic preservation for a type directed translation scheme of Featherweight Go

  2022cites this paper
• A relational theory of effects and coeffects

  2022cites this paper
• A type-directed, dictionary-passing translation of method overloading and structural subtyping in Featherweight Generic Go

  2022cites this paper
• Translation Certification for Smart Contracts

  2022cites this paper
• Program Equivalence in an Untyped, Call-by-value Lambda Calculus with Uncurried Recursive Functions

  2022cites this paper
• Step-Indexed Logical Relations for Nondeterministic and Probabilistic Choice

  2022cites this paper
• Fractional resources in unbounded separation logic

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

  2022cites this paper
• Plausible sealing for gradual parametricity

  2022cites this paper
• Reasoning about “reasoning about reasoning”: semantics and contextual equivalence for probabilistic programs with nested queries and recursion

  2022cites this paper
• Polarized Subtyping

  2022cites this paper
• A Type-Directed, Dictionary-Passing Translation of Featherweight Generic Go

  2022influential citation
• ADEV: Sound Automatic Differentiation of Expected Values of Probabilistic Programs

  2022cites this paper
• Direct Foundations for Compositional Programming

  2022cites this paper
• Automatic differentiation for ML-family languages: Correctness via logical relations

  2022influential citation
• Compositional optimizations for CertiCoq

  2021cites this paper
• Relational cost analysis in a functional-imperative setting

  2021cites this paper
• A Dictionary-Passing Translation of Featherweight Go

  2021cites this paper
• CPS transformation with affine types for call-by-value implicit polymorphism

  2021cites this paper
• Compiling with continuations, correctly

  2021cites this paper
• A Type-directed Operational Semantics Approach

  2021cites this paper
• DDUO: General-Purpose Dynamic Analysis for Differential Privacy

  2021cites this paper
• Abstraction Logic: The Marriage of Contextual Refinement and Separation Logic

  2021cites this paper
• Taming the Merge Operator

  2021cites this paper
• Verified efficient libraries for CakeML

  2020cites this paper
• Handling bidirectional control flow

  2020cites this paper
• Teaching Experience

  2020cites this paper
• Temporal Refinements for Guarded Recursive Types

  2020cites this paper
• Handling Bidirectional Control Flow: Technical Report

  2020cites this paper
• A Type-Directed Operational Semantics For a Calculus with a Merge Operator (Artifact)

  2020cites this paper
• Program equivalence for assisted grading of functional programs

  2020cites this paper
• Verified Optimizations for Functional Languages

  2020cites this paper
• On the Versatility of Open Logical Relations

  2020cites this paper
• Row and Bounded Polymorphism via Disjoint Polymorphism

  2020cites this paper
• Gradual System F

  2020cites this paper
• ReLoC Reloaded: A Mechanized Relational Logic for Fine-Grained Concurrency and Logical Atomicity

  2020cites this paper
• Coinductive Natural Semantics for Compiler Verification in Coq

  2020influential citation
• Hypernet semantics of programming languages

  2020cites this paper
• Incremental \lambda -Calculus in Cache-Transfer Style - Static Memoization by Program Transformation

  2019cites this paper
• Abstraction-safe effect handlers via tunneling

  2019cites this paper
• Formal Approaches to Secure Compilation

  2019cites this paper
• Binders by day, labels by night: effect instances via lexically scoped handlers

  2019cites this paper
• Under Control: Compositionally Correct Closure Conversion with Mutable State

  2019influential citation
• Gradual type theory

  2019cites this paper
• Binders by Day, Labels by Night

  2019cites this paper
• Distributive Disjoint Polymorphism for Compositional Programming

  2019cites this paper
• Polymorphic Relaxed Noninterference

  2019cites this paper
• Coherence of type class resolution

  2019cites this paper
• Fuzzi: a three-level logic for differential privacy

  2019cites this paper
• Designing Flexible, Modular Linguistic Abstractions

  2019cites this paper
• Data Abstraction and Relational Program Logic

  2019cites this paper
• in Cache-Transfer Style Static Memoization by Program Transformation

  2019cites this paper
• Compositional Non-Interference for Fine-Grained Concurrent Programs

  2019cites this paper
• The next 700 compiler correctness theorems (functional pearl)

  2019cites this paper
• THE VERIFIERS ? “ Can you trust your compiler ? ” So began

  2019influential citation
• The Next 700 Compiler Correctness Theorems (Functional Pearl)

  2019cites this paper
• On the expressiveness and semantics of information flow types

  2019cites this paper
• System FR: formalized foundations for the stainless verifier

  2019cites this paper
• Existential Types for Relaxed Noninterference

  2019cites this paper
• Program Equivalence for Algebraic Effects via Modalities

  2019cites this paper
• Relational cost analysis for functional-imperative programs

  2018cites this paper
• A case study in programming coinductive proofs: Howe’s method

  2018cites this paper
• Lecture Notes on Parametricity

  2018cites this paper
• 53 : 2 Type Abstraction for Relaxed Noninterference

  2018cites this paper
• 1 Formal Approaches to Secure Compilation

  2018cites this paper
• Reasoning about Polymorphic Manifest Contracts

  2018influential citation
• Gradual Type Theory (Extended Version)

  2018cites this paper
• Contextual equivalence for a probabilistic language with continuous random variables and recursion

  2018influential citation
• Graduality from embedding-projection pairs

  2018influential citation
• Types for Information Flow Control: Labeling Granularity and Semantic Models

  2018cites this paper
• Triangulating context lemmas

  2018cites this paper
• ReLoC: A Mechanised Relational Logic for Fine-Grained Concurrency

  2018cites this paper
• Compilación Certificada sobre Máquinas Abstractas de evaluación normal

  2017influential citation