package coq-lazy-pcf

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

Install

Dune Dependency

www.cs.bell-labs.com Edit opam file Versions (6)

Authors

  1. A
    Amy Felty
  2. J
    Jill Seaman

Maintainers

  1. H
    Hugo.Herbelin@inria.fr

Sources

v8.10.0.tar.gz
md5=a6021c336b12ce49e81b08164bbe01bc

Description

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: 07 Dec 2019

Dependencies (2)

  1. coq >= "8.10" & < "8.11~"
  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