Cited in
(only showing first 100 items - show all)- Towards Self-verification of HOL Light
- Sound global state caching for ALC with inverse roles
- scientific article; zbMATH DE number 1389649 (Why is no real title available?)
- Programs using syntax with first-class binders
- Context-free session type inference
- Types and programing languages
- Elements of discrete mathematics. Course, solved exercises, implementations with the languages Python and OCaml. With a preface by Gilles Dowek and Thérèse Hardin
- Single Assignment C: efficient support for high-level array operations in a functional setting
- Explicit effect subtyping
- Turning Inductive into Equational Specifications
- Optimal and cut-free tableaux for propositional dynamic logic with converse
- Improving parity games in practice
- Lightweight higher-kinded polymorphism
- An extended comparative study of language support for generic programming
- Contractive signatures with recursive types, type parameters, and abstract types
- Warnings for pattern matching
- Virtual-machine-based heterogeneous checkpointing
- Private Row Types: Abstracting the Unnamed
- Implementing hybrid semantics: from functional to imperative
- Designing and proving correct a convex hull algorithm with hypermaps in Coq
- Inferring expected runtimes of probabilistic integer programs using expected sizes
- A type system for reflective program generators
- Multi-stage programming with functors and monads: eliminating abstraction overhead from generic code
- Transactional events for ML
- Counterexample-guided partial bounding for recursive function synthesis
- From Sets to Bits in Coq
- scientific article; zbMATH DE number 1538025 (Why is no real title available?)
- A functional language to implement the divide-and-conquer Delaunay triangulation algorithm
- scientific article; zbMATH DE number 1222429 (Why is no real title available?)
- Symbolic analysis tools for CSP
- Tilings as a programming exercise.
- A flexible framework for visualisation of computational properties of general explicit substitutions calculi
- OCaml + XDuce
- Handlers in action
- Computer Science Logic
- Building reliable, high-performance networks with the Nuprl proof development system
- Well-founded coalgebras, revisited
- Applied semantics. International summer school, APPSEM 2000, Caminha, Portugal, September 9--15, 2000. Advanced lectures
- Semantic essence of AsmL
- Termination Proofs for Recursive Functions in FoCaLiZe
- Anti-patterns for rule-based languages
- General Decidability Results for Asynchronous Shared-Memory Programs: Higher-Order and Beyond
- Tree Components Programming: An Application to XML
- Adapting functional programs to higher order logic
- The coalgebraic class specification language CCSL
- scientific article; zbMATH DE number 5539366 (Why is no real title available?)
- scientific article; zbMATH DE number 1746460 (Why is no real title available?)
- Safe zero-cost coercions for Haskell
- Browndye: A software package for Brownian dynamics
- scientific article; zbMATH DE number 2090721 (Why is no real title available?)
- Algorithms and proofs inheritance in the FOC language
- Optimizing nested loops using local CPS conversion
- scientific article; zbMATH DE number 1942466 (Why is no real title available?)
- scientific article; zbMATH DE number 1954100 (Why is no real title available?)
- Semantics and algorithms for data-dependent grammars
- scientific article; zbMATH DE number 2087391 (Why is no real title available?)
- Lem: reusable engineering of real-world semantics
- scientific article; zbMATH DE number 1629943 (Why is no real title available?)
- A trusted mechanised JavaSript specification
- Matching and alpha-equivalence check for nominal terms
- scientific article; zbMATH DE number 1980941 (Why is no real title available?)
- A Coq library for internal verification of running-times
- Theorem Proving in Higher Order Logics
- Smart test data generators via logic programming
- Stream fusion, to completeness
- Verified characteristic formulae for CakeML
- Effekt: Capability-passing style for type- and effect-safe, extensible effect handlers in Scala
- Fiat: deductive synthesis of abstract data types in a proof assistant
- Chapar: certified causally consistent distributed key-value stores
- Programming Languages and Systems
- A proof dedicated meta-language
- The Isabelle collections framework
- Program verification by coinduction
- Delimited control in OCaml, abstractly and concretely
- Declarative foreign function binding through generic programming
- OCaml scientific computing. Functional programming in data science and artificial intelligence
- Semantics of typed lambda-calculus with constructors
- scientific article; zbMATH DE number 2009834 (Why is no real title available?)
- A constructive theory of continuous domains suitable for implementation
- Embedding an interpreted language using higher-order functions and types
- A simple library implementation of binary sessions
- Formal compiler construction in a logical framework
- Functional programming applied to scientific calculus. I: Numerical methods and applications
- A functional toolkit for morphological and phonological processing, application to a Sanskrit tagger
- Eliom: A Core ML Language for Tierless Web Programming
- \textsf{CC(X)}: semantic combination of congruence closure with solvable theories
- Zenon: An Extensible Automated Theorem Prover Producing Checkable Proofs
- LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description)
- Delimited dynamic binding
- More on balanced diets
- A formal semantics for protocol narrations
- FFT program generation for ring LWE-based cryptography
- Functional specification and prototyping with oriented combinatorial maps
- NESTED ALGORITHMIC SKELETONS FROM HIGHER ORDER FUNCTIONS
- Slothrop: Knuth-Bendix Completion with a Modern Termination Checker
- Model checking higher-order programs
- scientific article; zbMATH DE number 2090729 (Why is no real title available?)
- Polyhedral approximation of multivariate polynomials using Handelman's theorem
- Coinduction-based solution for minimization of Kripke structures
- scientific article; zbMATH DE number 2090072 (Why is no real title available?)
This page was built for software: OCaml
