OCaml

swMATH6363MaRDI QIDQ18489FDOQ18489

Author name not available (Why is that?)

Cited In (only showing first 100 items - show all)

• Single Assignment C: efficient support for high-level array operations in a functional setting
• Virtual-machine-based heterogeneous checkpointing
• Improving parity games in practice
• From Sets to Bits in Coq
• OCaml + XDuce
• Counterexample-guided partial bounding for recursive function synthesis
• Implementing Real Numbers With RZ
• Building reliable, high-performance networks with the Nuprl proof development system
• Tilings as a programming exercise.
• Termination Proofs for Recursive Functions in FoCaLiZe
• Applied semantics. International summer school, APPSEM 2000, Caminha, Portugal, September 9--15, 2000. Advanced lectures
• Anti-patterns for rule-based languages
• Adapting functional programs to higher order logic
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Theorem Proving in Higher Order Logics
• Programming Languages and Systems
• Matching and alpha-equivalence check for nominal terms
• Polyhedral Approximation of Multivariate Polynomials Using Handelman’s Theorem
• Title not available (Why is that?)
• A constructive theory of continuous domains suitable for implementation
• Formal compiler construction in a logical framework
• Title not available (Why is that?)
• NESTED ALGORITHMIC SKELETONS FROM HIGHER ORDER FUNCTIONS
• Dependency-style generic haskell
• Lightweight static capabilities
• Tool-assisted specification and verification of typed low-level languages
• Extending Coq with Imperative Features and Its Application to SAT Verification
• A verified proof checker for higher-order logic
• F-ing modules
• Customizing an XML-Haskell data binding with type isomorphism inference in generic Haskell
• Implementing nominal unification
• A type system for bounded space and functional in-place update
• Dependent types from counterexamples
• A Coq Library for Internal Verification of Running-Times
• Mathematical knowledge management in Foc
• Formalization of Wu's simple method in Coq
• Verifying distributed systems
• An operational semantics for object-oriented concepts based on the class hierarchy
• Verified Characteristic Formulae for CakeML
• Producing all ideals of a forest, functionally
• The Braga Method: Extracting Certified Algorithms from Complex Recursive Schemes in Coq
• Proceedings of the eleventh ACM SIGPLAN international conference on Functional programming
• An Interpretation of Isabelle/HOL in HOL Light
• Certifying properties of an efficient functional program for computing Gröbner bases
• Automatic Termination Verification for Higher-Order Functional Programs
• Certified Roundoff Error Bounds Using Semidefinite Programming
• Dependent types and multi-monadic effects in \(\mathrm{F}^*\)
• Programming languages and systems. 17th European symposium on programming, ESOP 2008, held as part of the joint European conferences on theory and practice of software, ETAPS 2008, Budapest, Hungary, March 29--April 6, 2008. Proceedings
• A Sound Semantics for OCaml light
• Proved Generation of Implementations from Computationally Secure Protocol Specifications
• A compact kernel for the calculus of inductive constructions
• A paraconsistent logic programming approach for querying inconsistent databases
• Inheritance-based subtyping
• Models of computation. An introduction to computability theory
• A probabilistic language based upon sampling functions
• Acute: High-level programming language design for distributed computation
• Programming Languages and Systems
• Title not available (Why is that?)
• A compiled implementation of strong reduction
• Static Analysis of String Manipulations in Critical Embedded C Programs
• Tilting at windmills with Coq: Formal verification of a compilation algorithm for parallel moves
• Towards automatic resource bound analysis for OCaml
• The foundation of self-developing blob machines for spatial computing
• Programming language concepts. With a chapter by Niels Hallenberg
• Amortized complexity verified
• Verifying the correctness and amortized complexity of a union-find implementation in separation logic with time credits
• Regular expression pattern matching for XML
• Turning Inductive into Equational Specifications
• Explicit effect subtyping
• Title not available (Why is that?)
• A functional language to implement the divide-and-conquer Delaunay triangulation algorithm
• General Decidability Results for Asynchronous Shared-Memory Programs: Higher-Order and Beyond
• Tree Components Programming: An Application to XML
• Title not available (Why is that?)
• Algorithms and proofs inheritance in the FOC language
• Optimizing nested loops using local CPS conversion
• Stream fusion, to completeness
• A proof dedicated meta-language
• A simple library implementation of binary sessions
• Program verification by coinduction
• Semantics of typed lambda-calculus with constructors
• OCaml scientific computing. Functional programming in data science and artificial intelligence
• Programs Using Syntax with First-Class Binders
• Context-Free Session Type Inference
• More on balanced diets
• A formal semantics for protocol narrations
• FFT program generation for ring LWE-based cryptography
• Implementing Hash-Consed Structures in Coq
• Experience of improving the BLAST static verification tool
• Proofs of a set of hybrid let-polymorphic type inference algorithms
• Compact bit encoding schemes for simply-typed lambda-terms
• Declarative Foreign Function Binding Through Generic Programming
• A Certified Constraint Solver over Finite Domains
• Implementing and reasoning about hash-consed data structures in Coq
• The First-Order Nominal Link
• Set-theoretic types for polymorphic variants
• On a monadic semantics for freshness
• Path resolution for nested recursive modules

This page was built for software: OCaml