ICFP（CCF B）（共 374 篇）
202639 篇 · 10(ICFP)
Machine-Generated, Machine-Checked Proofs for a Verified Compiler (Experience Report)
ICFP 10(ICFP)2026
Animated Pictures for Slide Presentations: From the Shallows to the Depths of a Domain-Specific Language (Functional Pearl)
ICFP 10(ICFP)2026
Safety First: How to Safely Disregard Unsafe Behaviour in Compiler Calculations
ICFP 10(ICFP)2026
Same Coeffect, Different Base: Connecting Two Dominant Approaches to Graded Types
ICFP 10(ICFP)2026
Package Managers à la Carte: A Formal Model of Dependency Resolution
ICFP 10(ICFP)2026
Citrus: Algebraic Reasoning about Superconductor Electronics
ICFP 10(ICFP)2026
First-Class Constrained Types: Elaboration, Type Inference, Approximation, and a Characterization of Termination
ICFP 10(ICFP)2026
Bimodels and Biorthogonality for Abstract Machines
ICFP 10(ICFP)2026
Editorial Message
ICFP 10(ICFP)2026
Compositional Neural-Cyber-Physical System Verification in the Interactive Theorem Prover of Your Choice
ICFP 10(ICFP)2026
Imprecise Probabilistic Programming, Precisely: Credal Sets via Graded Monads, BDDs, and Semiring-Parametric Inference (Functional Pearl)
ICFP 10(ICFP)2026
Misquoted No More: Securely Extracting F* Programs with IO
ICFP 10(ICFP)2026
Demand-on-Demand Control-Flow Analysis
ICFP 10(ICFP)2026
Assertions for Free: Transferring Invariants from Algorithm to Implementation Proofs (Functional Pearl)
ICFP 10(ICFP)2026
A Separation Logic for Parallel Time Complexity with Work and Span Credits
ICFP 10(ICFP)2026
Unscanning by Möbius Inversion (Functional Pearl)
ICFP 10(ICFP)2026
HMCFA: A Precise and Practical Big-Step Control Flow Analysis for Effect Handlers
ICFP 10(ICFP)2026
Towards a Higher-Order Bialgebraic Denotational Semantics
ICFP 10(ICFP)2026
QuickChecking Convergence of Rewriting Systems (Functional Pearl)
ICFP 10(ICFP)2026
LoCalMem: Type-Directed Adaptive Serialization for Location- and Content-Addressable Memory
ICFP 10(ICFP)2026
On Recursion in Graded Modal Type Theory
ICFP 10(ICFP)2026
Compositional Generator Equivalence
ICFP 10(ICFP)2026
Tail Modulo Async-Await
ICFP 10(ICFP)2026
Mode Crossing
ICFP 10(ICFP)2026
Confluence Techniques for Dependent Type Theory with Typed Conversion
ICFP 10(ICFP)2026
A Catenable, Splittable, Transient Sequence Data Structure
ICFP 10(ICFP)2026
Proofs Promptly: Proof-Oriented Programming with AI Agents (Experience Report)
ICFP 10(ICFP)2026
LazyHMC: Hamiltonian Monte Carlo Simulation for Lazy, Infinite Dimensional Probabilistic Programs
ICFP 10(ICFP)2026
Let It Be Optimized: Building Multi-stage Evaluators with Let-Insertion and Optimizations in Small Pieces (Functional Pearl)
ICFP 10(ICFP)2026
Adequacy for Predicate Transformer Semantics
ICFP 10(ICFP)2026
Inlining as a Space Optimization: A Simple Time- and Space-Invariant Implementation of the Weak Lambda-Calculus
ICFP 10(ICFP)2026
An Equational and Graphical Fixed-Point Calculus (Functional Pearl)
ICFP 10(ICFP)2026
Completeness of Iris-Based Program Logics
ICFP 10(ICFP)2026
Programmable Property-Based Testing
ICFP 10(ICFP)2026
Another Type Inference Algorithm for First-Class Implicit Polymorphism
ICFP 10(ICFP)2026
When Types Intersect and Effects Get Handled
ICFP 10(ICFP)2026
RunbookFX: Type- and Effect-Safe LLM Synthesis for Executable Incident Diagnosis and Mitigation
ICFP 10(ICFP)2026
Programming Backpropagation with Reverse Handlers for Arrows
ICFP 10(ICFP)2026
Set-Theoretic Types for Erlang in Practice (Experience Report)
ICFP 10(ICFP)2026
202536 篇 · 9(ICFP)
Fusing Session-Typed Concurrent Programming into Functional Programming
ICFP 9(ICFP)2025
Robust Dynamic Embedding for Gradual Typing
ICFP 9(ICFP)2025
Big Steps in Higher-Order Mathematical Operational Semantics
ICFP 9(ICFP)2025
Verified Interpreters for Dynamic Languages with Applications to the Nix Expression Language
ICFP 9(ICFP)2025
A Haskell Adiabatic DSL: Solving Classical Optimization Problems on Quantum Hardware
ICFP 9(ICFP)2025
Multiple Resumptions and Local Mutable State, Directly
ICFP 9(ICFP)2025
SecRef*: Securely Sharing Mutable References between Verified and Unverified Code in F*
ICFP 9(ICFP)2025
Almost Fair Simulations
ICFP 9(ICFP)2025
Frex: Dependently Typed Algebraic Simplification
ICFP 9(ICFP)2025
Truly Functional Solutions to the Longest Uptrend Problem (Functional Pearl)
ICFP 9(ICFP)2025
Reasoning about Weak Isolation Levels in Separation Logic
ICFP 9(ICFP)2025
Multi-stage Programming with Splice Variables
ICFP 9(ICFP)2025
Type Theory in Type Theory using a Strictified Syntax
ICFP 9(ICFP)2025
Polynomial-Time Program Equivalence for Machine Knitting
ICFP 9(ICFP)2025
Normalization by Evaluation for Non-cumulativity
ICFP 9(ICFP)2025
Type Universes as Kripke Worlds
ICFP 9(ICFP)2025
Effectful Lenses: There and Back with Different Monads
ICFP 9(ICFP)2025
Modular Reasoning about Error Bounds for Concurrent Probabilistic Programs
ICFP 9(ICFP)2025
Verifying Graph Algorithms in Separation Logic: A Case for an Algebraic Approach
ICFP 9(ICFP)2025
Linear Types with Dynamic Multiplicities in Dependent Type Theory (Functional Pearl)
ICFP 9(ICFP)2025
2-Functoriality of Initial Semantics, and Applications
ICFP 9(ICFP)2025
Formal Semantics and Program Logics for a Fragment of OCaml
ICFP 9(ICFP)2025
First-Order Laziness
ICFP 9(ICFP)2025
Call-Guarded Abstract Definitional Interpreters
ICFP 9(ICFP)2025
Relax! The Semilenient Core of Choreographic Programming (Functional Pearl)
ICFP 9(ICFP)2025
Functional Networking for Millions of Docker Desktops (Experience Report)
ICFP 9(ICFP)2025
Bialgebraic Reasoning on Stateful Languages
ICFP 9(ICFP)2025
Correctness Meets Performance: From Agda to Futhark
ICFP 9(ICFP)2025
Pushing the Information-Theoretic Limits of Random Access Lists: Traversing Cons Lists in (1 + 1/𝜎 ) ⌊lg 𝑛⌋ + 𝜎 + 9 Steps
ICFP 9(ICFP)2025
CRDT Emulation, Simulation, and Representation Independence
ICFP 9(ICFP)2025
Fulls Seldom Differ
ICFP 9(ICFP)2025
Environment-Sharing Analysis and Caller-Provided Environments for Higher-Order Languages
ICFP 9(ICFP)2025
McTT: A Verified Kernel for a Proof Assistant
ICFP 9(ICFP)2025
A Bargain for Mergesorts: How to Prove Your Mergesort Correct and Stable, Almost for Free
ICFP 9(ICFP)2025
Compiling with Generating Functions
ICFP 9(ICFP)2025
Teaching Software Specification (Experience Report)
ICFP 9(ICFP)2025
202435 篇 · 8(ICFP)
Error Credits: Resourceful Reasoning about Error Bounds for Higher-Order Probabilistic Programs
ICFP 8(ICFP)2024引用 23
Oxidizing OCaml with Modal Memory Management
ICFP 8(ICFP)2024引用 22
Sound Borrow-Checking for Rust via Symbolic Semantics
ICFP 8(ICFP)2024引用 14
A Two-Phase Infinite/Finite Low-Level Memory Model: Reconciling Integer–Pointer Casts, Finite Space, and undef at the LLVM IR Level of Abstraction
ICFP 8(ICFP)2024引用 11
CCLemma: E-Graph Guided Lemma Discovery for Inductive Equational Proofs
ICFP 8(ICFP)2024引用 11
Dependent Ghosts Have a Reflection for Free
ICFP 8(ICFP)2024引用 9
A Coq Mechanization of JavaScript Regular Expression Semantics
ICFP 8(ICFP)2024引用 8
Almost-Sure Termination by Guarded Refinement
ICFP 8(ICFP)2024引用 7
Snapshottable Stores
ICFP 8(ICFP)2024引用 7
Abstracting Effect Systems for Algebraic Effect Handlers
ICFP 8(ICFP)2024引用 7
Automated Verification of Higher-Order Probabilistic Programs via a Dependent Refinement Type System
ICFP 8(ICFP)2024引用 7
Compiled, Extensible, Multi-language DSLs (Functional Pearl)
ICFP 8(ICFP)2024引用 7
Abstract Interpreters: A Monadic Approach to Modular Verification
ICFP 8(ICFP)2024引用 6
Closure-Free Functional Programming in a Two-Level Type Theory
ICFP 8(ICFP)2024引用 5
Story of Your Lazy Function’s Life: A Bidirectional Demand Semantics for Mechanized Cost Analysis of Lazy Programs
ICFP 8(ICFP)2024引用 5
Synchronous Programming with Refinement Types
ICFP 8(ICFP)2024引用 5
Staged Compilation with Module Functors
ICFP 8(ICFP)2024引用 4
Contextual Typing
ICFP 8(ICFP)2024引用 4
How to Bake a Quantum Π
ICFP 8(ICFP)2024引用 3
Deriving with Derivatives: Optimizing Incremental Fixpoints for Higher-Order Flow Analysis
ICFP 8(ICFP)2024引用 3
A Safe Low-Level Language for Computer Algebra and Its Formally Verified Compiler
ICFP 8(ICFP)2024引用 2
Double-Ended Bit-Stealing for Algebraic Data Types
ICFP 8(ICFP)2024引用 2
Parallel Algebraic Effect Handlers
ICFP 8(ICFP)2024引用 2
Grokking the Sequent Calculus (Functional Pearl)
ICFP 8(ICFP)2024引用 2
Functional Programming in Financial Markets (Experience Report)
ICFP 8(ICFP)2024引用 2
Example-Based Reasoning about the Realizability of Polymorphic Programs
ICFP 8(ICFP)2024引用 1
Specification and Verification for Unrestricted Algebraic Effects and Handling
ICFP 8(ICFP)2024引用 1
Refinement Composition Logic
ICFP 8(ICFP)2024引用 1
Blame-Correct Support for Receiver Properties in Recursively-Structured Actor Contracts
ICFP 8(ICFP)2024引用 1
The Functional, the Imperative, and the Sudoku: Getting Good, Bad, and Ugly to Get Along (Functional Pearl)
ICFP 8(ICFP)2024引用 1
The Long Way to Deforestation: A Type Inference and Elaboration Technique for Removing Intermediate Data Structures
ICFP 8(ICFP)2024
On the Operational Theory of the CPS-Calculus: Towards a Theoretical Foundation for IRs
ICFP 8(ICFP)2024
Beyond Trees: Calculating Graph-Based Compilers (Functional Pearl)
ICFP 8(ICFP)2024
Call-by-Unboxed-Value
ICFP 8(ICFP)2024
Gradual Indexed Inductive Types
ICFP 8(ICFP)2024
202333 篇 · 7(ICFP)
Intrinsically Typed Sessions with Callbacks (Functional Pearl)
ICFP 7(ICFP)2023
Embedding by Unembedding
ICFP 7(ICFP)2023
Asynchronous Modal FRP
ICFP 7(ICFP)2023
Dependently-Typed Programming with Logical Equality Reflection
ICFP 7(ICFP)2023
Flexible Instruction-Set Semantics via Abstract Monads (Experience Report)
ICFP 7(ICFP)2023
Formal Specification and Testing for Reinforcement Learning
ICFP 7(ICFP)2023
What Happens When Students Switch (Functional) Languages (Experience Report)
ICFP 7(ICFP)2023
Etna: An Evaluation Platform for Property-Based Testing (Experience Report)
ICFP 7(ICFP)2023
Verifying Reliable Network Components in a Distributed Separation Logic with Dependent Separation Protocols
ICFP 7(ICFP)2023
Timely Computation
ICFP 7(ICFP)2023
A General Fine-Grained Reduction Theory for Effect Handlers
ICFP 7(ICFP)2023
Trustworthy Runtime Verification via Bisimulation (Experience Report)
ICFP 7(ICFP)2023
Generic Programming with Extensible Data Types: Or, Making Ad Hoc Extensible Data Types Less Ad Hoc
ICFP 7(ICFP)2023
Special Delivery: Programming with Mailbox Types
ICFP 7(ICFP)2023
Modularity, Code Specialization, and Zero-Cost Abstractions for Program Verification
ICFP 7(ICFP)2023
Modular Models of Monoids with Operations
ICFP 7(ICFP)2023
Higher-Order Property-Directed Reachability
ICFP 7(ICFP)2023
Combinator-Based Fixpoint Algorithms for Big-Step Abstract Interpreters
ICFP 7(ICFP)2023
Calculating Compilers for Concurrency
ICFP 7(ICFP)2023
More Fixpoints! (Functional Pearl)
ICFP 7(ICFP)2023
A Graded Modal Dependent Type Theory with a Universe and Erasure, Formalized
ICFP 7(ICFP)2023
FP²: Fully in-Place Functional Programming
ICFP 7(ICFP)2023
How to Evaluate Blame for Gradual Types, Part 2
ICFP 7(ICFP)2023
Bit-Stealing Made Legal: Compilation for Custom Memory Representations of Algebraic Data Types
ICFP 7(ICFP)2023
HasChor: Functional Choreographic Programming for All (Functional Pearl)
ICFP 7(ICFP)2023
MacoCaml: Staging Composable and Compilable Macros
ICFP 7(ICFP)2023
The Verse Calculus: A Core Calculus for Deterministic Functional Logic Programming
ICFP 7(ICFP)2023
Dependent Session Protocols in Separation Logic from First Principles (Functional Pearl)
ICFP 7(ICFP)2023
Reflecting on Random Generation
ICFP 7(ICFP)2023
Explicit Refinement Types
ICFP 7(ICFP)2023
LURK: Lambda, the Ultimate Recursive Knowledge (Experience Report)
ICFP 7(ICFP)2023
Typing Records, Maps, and Structs
ICFP 7(ICFP)2023
With or Without You: Programming with Effect Exclusion
ICFP 7(ICFP)2023
202235 篇 · 6(ICFP)
Random testing of a higher-order blockchain language (experience report)
ICFP 6(ICFP)2022
Beyond Relooper: recursive translation of unstructured control flow to structured control flow (functional pearl)
ICFP 6(ICFP)2022
Formal reasoning about layered monadic interpreters
ICFP 6(ICFP)2022
Analyzing binding extent in 3CPS
ICFP 6(ICFP)2022
Staged compilation with two-level type theory
ICFP 6(ICFP)2022
Introduction and elimination, left and right
ICFP 6(ICFP)2022
Multiparty GV: functional multiparty session types with certified deadlock freedom
ICFP 6(ICFP)2022
Multi types and reasonable space
ICFP 6(ICFP)2022
On Feller continuity and full abstraction
ICFP 6(ICFP)2022
The theory of call-by-value solvability
ICFP 6(ICFP)2022
Modular probabilistic models via algebraic effects
ICFP 6(ICFP)2022
A reasonably gradual type theory
ICFP 6(ICFP)2022
Propositional equality for gradual dependently typed programming
ICFP 6(ICFP)2022
‘do’ unchained: embracing local imperativity in a purely functional language (functional pearl)
ICFP 6(ICFP)2022
Datatype-generic programming meets elaborator reflection
ICFP 6(ICFP)2022
Entanglement detection with near-zero cost
ICFP 6(ICFP)2022
Structural versus pipeline composition of higher-order functions (experience report)
ICFP 6(ICFP)2022
Reference counting with frame limited reuse
ICFP 6(ICFP)2022
Verified symbolic execution with Kripke specification monads (and no meta-programming)
ICFP 6(ICFP)2022
Aeneas: Rust verification by functional translation
ICFP 6(ICFP)2022
Constraint-based type inference for FreezeML
ICFP 6(ICFP)2022
Linearly qualified types: generic inference for capabilities and uniqueness
ICFP 6(ICFP)2022
Flexible presentations of graded monads
ICFP 6(ICFP)2022
Searching entangled program spaces
ICFP 6(ICFP)2022
Practical generic programming over a universe of native datatypes
ICFP 6(ICFP)2022
Safe couplings: coupled refinement types
ICFP 6(ICFP)2022
Generating circuits with generators
ICFP 6(ICFP)2022
A completely unique account of enumeration
ICFP 6(ICFP)2022
A simple and efficient implementation of strong call by need by an abstract machine
ICFP 6(ICFP)2022
Monadic compiler calculation (functional pearl)
ICFP 6(ICFP)2022
Automatically deriving control-flow graph generators from operational semantics
ICFP 6(ICFP)2022
Later credits: resourceful reasoning for the later modality
ICFP 6(ICFP)2022
Program adverbs and Tlön embeddings
ICFP 6(ICFP)2022
Fusing industry and academia at GitHub (experience report)
ICFP 6(ICFP)2022
Normalization for fitch-style modal calculi
ICFP 6(ICFP)2022
202135 篇 · 5(ICFP)
Automatic amortized resource analysis with the Quantum physicist’s method
ICFP 5(ICFP)2021
Steel: proof-oriented programming in a dependently typed concurrent separation logic
ICFP 5(ICFP)2021
How to evaluate blame for gradual types
ICFP 5(ICFP)2021
Catala: a programming language for the law
ICFP 5(ICFP)2021
Getting to the point: index sets and parallelism-preserving autodiff for pointful array programming
ICFP 5(ICFP)2021
Compositional optimizations for CertiCoq
ICFP 5(ICFP)2021
Theorems for free from separation logic specifications
ICFP 5(ICFP)2021
Contextual modal types for algebraic effects and handlers
ICFP 5(ICFP)2021
A theory of higher-order subtyping with type intervals
ICFP 5(ICFP)2021
Efficient tree-traversals: reconciling parallelism and dense data representations
ICFP 5(ICFP)2021
Propositions-as-types and shared state
ICFP 5(ICFP)2021
Grafs: declarative graph analytics
ICFP 5(ICFP)2021
Reasoning about the garden of forking paths
ICFP 5(ICFP)2021
Calculating dependently-typed compilers (functional pearl)
ICFP 5(ICFP)2021
Newly-single and loving it: improving higher-order must-alias analysis with heap fragments
ICFP 5(ICFP)2021
Certifying the synthesis of heap-manipulating programs
ICFP 5(ICFP)2021
Modular, compositional, and executable formal semantics for LLVM IR
ICFP 5(ICFP)2021
Deriving efficient program transformations from rewrite rules
ICFP 5(ICFP)2021
An existential crisis resolved: type inference for first-class existential types
ICFP 5(ICFP)2021
Symbolic and automatic differentiation of languages
ICFP 5(ICFP)2021
GhostCell: separating permissions from data in Rust
ICFP 5(ICFP)2021
On continuation-passing transformations and expected cost analysis
ICFP 5(ICFP)2021
Of JavaScript AOT compilation performance
ICFP 5(ICFP)2021
CPS transformation with affine types for call-by-value implicit polymorphism
ICFP 5(ICFP)2021
Generalized evidence passing for effect handlers: efficient compilation of effect handlers to C
ICFP 5(ICFP)2021
Persistent software transactional memory in Haskell
ICFP 5(ICFP)2021
Formal verification of a concurrent bounded queue in a weak memory model
ICFP 5(ICFP)2021
An order-aware dataflow model for parallel Unix pipelines
ICFP 5(ICFP)2021
Higher-order probabilistic adversarial computations: categorical semantics and program logics
ICFP 5(ICFP)2021
Algebras for weighted search
ICFP 5(ICFP)2021
Client-server sessions in linear logic
ICFP 5(ICFP)2021
Distributing intersection and union types with splits and duality (functional pearl)
ICFP 5(ICFP)2021
ProbNV: probabilistic verification of network control planes
ICFP 5(ICFP)2021
Skipping the binder bureaucracy with mixed embeddings in a semantics course (functional pearl)
ICFP 5(ICFP)2021
Reasoning about effect interaction by fusion
ICFP 5(ICFP)2021
202037 篇 · 4(ICFP)
Achieving high-performance the functional way: a functional pearl on expressing high-performance optimizations as rewrite strategies
ICFP 4(ICFP)2020引用 58
A unified view of modalities in type systems
ICFP 4(ICFP)2020引用 52
Program sketching with live bidirectional evaluation
ICFP 4(ICFP)2020引用 50
Retrofitting parallelism onto OCaml
ICFP 4(ICFP)2020引用 41
Raising expectations: automating expected cost analysis with types
ICFP 4(ICFP)2020引用 39
The simple essence of algebraic subtyping: principal type inference with subtyping made easy (functional pearl)
ICFP 4(ICFP)2020引用 35
Separation logic for sequential programs (functional pearl)
ICFP 4(ICFP)2020引用 34
Effect handlers, evidently
ICFP 4(ICFP)2020引用 33
A quick look at impredicativity
ICFP 4(ICFP)2020引用 32
SteelCore: an extensible concurrent separation logic for effectful dependently typed programs
ICFP 4(ICFP)2020引用 31
Compiling effect handlers in capability-passing style
ICFP 4(ICFP)2020引用 29
Liquid information flow control
ICFP 4(ICFP)2020引用 26
Cosmo: a concurrent separation logic for multicore OCaml
ICFP 4(ICFP)2020引用 24
Scala step-by-step: soundness for DOT with step-indexed logical relations in Iris
ICFP 4(ICFP)2020引用 22
A general approach to define binders using matching logic
ICFP 4(ICFP)2020引用 21
Staged selective parser combinators
ICFP 4(ICFP)2020引用 20
Denotational recurrence extraction for amortized analysis
ICFP 4(ICFP)2020引用 20
Composing and decomposing op-based CRDTs with semidirect products
ICFP 4(ICFP)2020引用 17
TLC: temporal logic of distributed components
ICFP 4(ICFP)2020引用 16
Recovering purity with comonads and capabilities
ICFP 4(ICFP)2020引用 15
Liquid resource types
ICFP 4(ICFP)2020引用 14
Regular language type inference with term rewriting
ICFP 4(ICFP)2020引用 12
Kinds are calling conventions
ICFP 4(ICFP)2020引用 11
Lower your guards: a compositional pattern-match coverage checker
ICFP 4(ICFP)2020引用 10
Kindly bent to free us
ICFP 4(ICFP)2020引用 10
A dependently typed calculus with pattern matching and erasure inference
ICFP 4(ICFP)2020引用 9
Elaboration with first-class implicit function types
ICFP 4(ICFP)2020引用 8
Stable relations and abstract interpretation of higher-order programs
ICFP 4(ICFP)2020引用 7
Effects for efficiency: asymptotic speedup with first-class control
ICFP 4(ICFP)2020引用 6
Parsing with zippers (functional pearl)
ICFP 4(ICFP)2020引用 5
Higher-order demand-driven symbolic evaluation
ICFP 4(ICFP)2020引用 5
Computation focusing
ICFP 4(ICFP)2020引用 4
Sealing pointer-based optimizations behind pure functions
ICFP 4(ICFP)2020引用 4
Strong functional pearl: Harper’s regular-expression matcher in Cedille
ICFP 4(ICFP)2020引用 3
Duplo: a framework for OCaml post-link optimisation
ICFP 4(ICFP)2020引用 2
Sparcl: a language for partially-invertible computation
ICFP 4(ICFP)2020
Signature restriction for polymorphic algebraic effects
ICFP 4(ICFP)2020
201939 篇 · 3(ICFP)
Call-by-need is clairvoyant call-by-value
ICFP 3(ICFP)2019
Relational cost analysis for functional-imperative programs
ICFP 3(ICFP)2019
From high-level inference algorithms to efficient code
ICFP 3(ICFP)2019
Dependently typed Haskell in industry (experience report)
ICFP 3(ICFP)2019
A reasonably exceptional type theory
ICFP 3(ICFP)2019
Lambda: the ultimate sublanguage (experience report)
ICFP 3(ICFP)2019
An efficient algorithm for type-safe structural diffing
ICFP 3(ICFP)2019
Equations reloaded: high-level dependently-typed functional programming and proving in Coq
ICFP 3(ICFP)2019
Demystifying differentiable programming: shift/reset the penultimate backpropagator
ICFP 3(ICFP)2019
Quantitative program reasoning with graded modal types
ICFP 3(ICFP)2019
Higher-order type-level programming in Haskell
ICFP 3(ICFP)2019
Compiling with continuations, or without? whatever.
ICFP 3(ICFP)2019
Fairness in responsive parallelism
ICFP 3(ICFP)2019
Mixed linear and non-linear recursive types
ICFP 3(ICFP)2019
Teaching the art of functional programming using automated grading (experience report)
ICFP 3(ICFP)2019
Simply RaTT: a fitch-style modal calculus for reactive programming without space leaks
ICFP 3(ICFP)2019
Synthesizing differentially private programs
ICFP 3(ICFP)2019
Approximate normalization for gradual dependent types
ICFP 3(ICFP)2019
Selective applicative functors
ICFP 3(ICFP)2019
Mechanized relational verification of concurrent programs with continuations
ICFP 3(ICFP)2019
Sound and robust solid modeling via exact real arithmetic and continuity
ICFP 3(ICFP)2019
Simple noninterference from parametricity
ICFP 3(ICFP)2019
Rebuilding racket on chez scheme (experience report)
ICFP 3(ICFP)2019
A role for dependent types in Haskell
ICFP 3(ICFP)2019
The next 700 compiler correctness theorems (functional pearl)
ICFP 3(ICFP)2019
Sequential programming for replicated data stores
ICFP 3(ICFP)2019
Closure conversion is safe for space
ICFP 3(ICFP)2019
Implementing a modal dependent type theory
ICFP 3(ICFP)2019
Linear capabilities for fully abstract compilation of separation-logic-verified code
ICFP 3(ICFP)2019
Cubical agda: a dependently typed programming language with univalence and higher inductive types
ICFP 3(ICFP)2019
Dijkstra monads for all
ICFP 3(ICFP)2019
Fuzzi: a three-level logic for differential privacy
ICFP 3(ICFP)2019
Coherence of type class resolution
ICFP 3(ICFP)2019
Efficient differentiable programming in a functional array-processing language
ICFP 3(ICFP)2019
Lambda calculus with algebraic simplification for reduction parallelization by equational reasoning
ICFP 3(ICFP)2019
A predicate transformer semantics for effects (functional pearl)
ICFP 3(ICFP)2019
Narcissus: correct-by-construction derivation of decoders and encoders from binary formats
ICFP 3(ICFP)2019
Synthesizing symmetric lenses
ICFP 3(ICFP)2019
A mechanical formalization of higher-ranked polymorphic type inference
ICFP 3(ICFP)2019
201840 篇 · 2(ICFP)
Build systems à la carte
ICFP 2(ICFP)2018
Functional programming for modular Bayesian inference
ICFP 2(ICFP)2018
Teaching how to program using automated assessment and functional glossy games (experience report)
ICFP 2(ICFP)2018
Mtac2: typed tactics for backward reasoning in Coq
ICFP 2(ICFP)2018
Tight typings and split bounds
ICFP 2(ICFP)2018
Fault tolerant functional reactive programming (functional pearl)
ICFP 2(ICFP)2018
Static interpretation of higher-order modules in Futhark: functional GPU programming in the large
ICFP 2(ICFP)2018
MoSeL: a general, extensible modal framework for interactive proofs in separation logic
ICFP 2(ICFP)2018
Incremental relational lenses
ICFP 2(ICFP)2018
Prototyping a functional language using higher-order logic programming: a functional pearl on learning the ways of λProlog/Makam
ICFP 2(ICFP)2018
Contextual equivalence for a probabilistic language with continuous random variables and recursion
ICFP 2(ICFP)2018
Ready, set, verify! applying hs-to-coq to real-world Haskell code (experience report)
ICFP 2(ICFP)2018
Keep your laziness in check
ICFP 2(ICFP)2018
Merlin: a language server for OCaml (experience report)
ICFP 2(ICFP)2018
A type and scope safe universe of syntaxes with binding: their semantics and proofs
ICFP 2(ICFP)2018
Equivalences for free: univalent parametricity for effective transport
ICFP 2(ICFP)2018
Synthesizing quotient lenses
ICFP 2(ICFP)2018
Partially-static data as free extension of algebras
ICFP 2(ICFP)2018
Versatile event correlation with algebraic effects
ICFP 2(ICFP)2018
Casts and costs: harmonizing safety and performance in gradual typing
ICFP 2(ICFP)2018
Refunctionalization of abstract abstract machines: bridging the gap between abstract abstract machines and abstract definitional interpreters (functional pearl)
ICFP 2(ICFP)2018
What’s the difference? a functional pearl on subtracting bijections
ICFP 2(ICFP)2018
Relational algebra by way of adjunctions
ICFP 2(ICFP)2018
Functional programming for compiling and decompiling computer-aided design
ICFP 2(ICFP)2018
Elaborating dependent (co)pattern matching
ICFP 2(ICFP)2018
A spectrum of type soundness and performance
ICFP 2(ICFP)2018
What you needa know about Yoneda: profunctor optics and the Yoneda lemma (functional pearl)
ICFP 2(ICFP)2018
Capturing the future by replaying the past (functional pearl)
ICFP 2(ICFP)2018
Generic zero-cost reuse for dependent types
ICFP 2(ICFP)2018
Handling delimited continuations with dependent types
ICFP 2(ICFP)2018
Parallel complexity analysis with temporal session types
ICFP 2(ICFP)2018
Graduality from embedding-projection pairs
ICFP 2(ICFP)2018
Strict and lazy semantics for effects: layering monads and comonads
ICFP 2(ICFP)2018
Compositional soundness proofs of abstract interpreters
ICFP 2(ICFP)2018
Generic deriving of generic traversals
ICFP 2(ICFP)2018
Competitive parallelism: getting your priorities right
ICFP 2(ICFP)2018
Reasonably programmable literal notation
ICFP 2(ICFP)2018
Finitary polymorphism for optimizing type-directed compilation
ICFP 2(ICFP)2018
Parametric polymorphism and operational improvement
ICFP 2(ICFP)2018
The simple essence of automatic differentiation
ICFP 2(ICFP)2018
201745 篇 · 1(ICFP)
Verified low-level programming embedded in F*
ICFP 1(ICFP)2017引用 172
Kami: a platform for high-level parametric hardware specification and its modular verification
ICFP 1(ICFP)2017引用 128
A metaprogramming framework for formal verification
ICFP 1(ICFP)2017引用 101
Manifest sharing with session types
ICFP 1(ICFP)2017引用 83
On the expressive power of user-defined effects: effect handlers, monadic reflection, delimited control
ICFP 1(ICFP)2017引用 81
Theorems for free for free: parametricity, with and without types
ICFP 1(ICFP)2017引用 64
Gradual typing with union and intersection types
ICFP 1(ICFP)2017引用 62
A specification for dependent types in Haskell
ICFP 1(ICFP)2017引用 61
A relational logic for higher-order programs
ICFP 1(ICFP)2017引用 57
Abstracting definitional interpreters (functional pearl)
ICFP 1(ICFP)2017引用 57
Parametric quantifiers for dependent type theory
ICFP 1(ICFP)2017引用 57
A framework for adaptive differential privacy
ICFP 1(ICFP)2017引用 51
On polymorphic gradual typing
ICFP 1(ICFP)2017引用 47
Compiling to categories
ICFP 1(ICFP)2017引用 43
Effect-driven QuickChecking of compilers
ICFP 1(ICFP)2017引用 37
Normalization by evaluation for sized dependent types
ICFP 1(ICFP)2017引用 37
A unified approach to solving seven programming problems (functional pearl)
ICFP 1(ICFP)2017引用 35
Automating sized-type inference for complexity analysis
ICFP 1(ICFP)2017引用 35
Staged generic programming
ICFP 1(ICFP)2017引用 34
Foundations of strong call by need
ICFP 1(ICFP)2017引用 30
Imperative functional programs that explain their work
ICFP 1(ICFP)2017引用 25
Testing and debugging functional reactive programming
ICFP 1(ICFP)2017引用 23
Local refinement typing
ICFP 1(ICFP)2017引用 22
Whip: higher-order contracts for modern services
ICFP 1(ICFP)2017引用 20
Verifying efficient function calls in CakeML
ICFP 1(ICFP)2017引用 19
How to prove your calculus is decidable: practical applications of second-order algebraic theories and computation
ICFP 1(ICFP)2017引用 18
Persistence for the masses: RRB-vectors in a systems language
ICFP 1(ICFP)2017引用 18
Chaperone contracts for higher-order sessions
ICFP 1(ICFP)2017引用 16
Scaling up functional programming education: under the hood of the OCaml MOOC
ICFP 1(ICFP)2017引用 14
Super 8 languages for making movies (functional pearl)
ICFP 1(ICFP)2017引用 13
Constrained type families
ICFP 1(ICFP)2017引用 11
SpaceSearch: a library for building and verifying solver-aided tools
ICFP 1(ICFP)2017引用 9
Symbolic conditioning of arrays in probabilistic programs
ICFP 1(ICFP)2017引用 9
Inferring scope through syntactic sugar
ICFP 1(ICFP)2017引用 8
Visitors unchained
ICFP 1(ICFP)2017引用 8
Generic functional parallel algorithms: scan and FFT
ICFP 1(ICFP)2017引用 7
A pretty but not greedy printer (functional pearl)
ICFP 1(ICFP)2017引用 6
Prototyping a query compiler using Coq (experience report)
ICFP 1(ICFP)2017引用 6
Lock-step simulation is child's play (experience report)
ICFP 1(ICFP)2017引用 4
Faster coroutine pipelines
ICFP 1(ICFP)2017引用 4
Better living through operational semantics: an optimizing compiler for radio protocols
ICFP 1(ICFP)2017引用 3
No-brainer CPS conversion (functional pearl)
ICFP 1(ICFP)2017引用 1
Herbarium Racketensis: a stroll through the woods (functional pearl)
ICFP 1(ICFP)2017引用 1
Gradual session types
ICFP 1(ICFP)2017
Editorial message
ICFP 1(ICFP)2017