package coq-lazy-pcf

  1. Overview
  2. Homepage
Subject Reduction for Lazy-PCF

Install

Dune Dependency

github.com Edit opam file Versions (6)

Authors

  1. A
    Amy Felty
  2. J
    Jill Seaman

Maintainers

  1. H
    Hugo.Herbelin@inria.fr

Sources

v8.6.0.tar.gz
md5=be16a0d7429e56bddb5be5340f65cefb

Description

http://www.cs.bell-labs.com/~felty/abstracts/ppcoq.html

An Operational Semantics of Lazy Evaluation and a Proof of Subject Reduction

Tags

keyword: functional programming keyword: lazy evaluation keyword: operational semantics keyword: type soundness keyword: normal forms category: Computer Science/Lambda Calculi

Published: 20 Nov 2018

Dependencies (2)

  1. coq >= "8.6" & < "8.7~"
  2. ocaml

Dev Dependencies

None

Used by

None

Conflicts

None

Rocq

Interactive Theorem Prover

Zulip GitHub Discourse Mastodon RSS
About
Changelog Releases Industrial Users Academic Users History Why Rocq? Roadmap
Ecosystem
Platform Packages Rocq Team Community Consortium Events Rocq Planet Jobs
Resources
Install Rocq Get Started Documentation Books Papers Logo
Policies
Governance Privacy Code of Conduct