Artifact associated with Consistency of a Dependent Calculus of Indistinguishability

integration_instructionsResearch softwarekeyboard_double_arrow_right Software 14 Oct 2024 English Publisher:ZenodoFunded by:NSF | SHF: SMALL:Dependency Tra..., NSF | SHF: Small: Mechanized re...

Authors: Liu, Yiyun; Chan, Jonathan; Weirich, Stephanie;

doi: 10.5281/zenodo.13930551 , 10.5281/zenodo.14252132 , 10.5281/zenodo.13930550 , 10.5281/zenodo.14201563

Artifact associated with Consistency of a Dependent Calculus of Indistinguishability

- Summary
- Metrics

Abstract

The artifact contains the mechanized Coq proof and a prototype typechecker for the calculus described in the paper "Consistency of a Dependent Calculus of Indistinguishability". In addition to the source code, the artifact includes a virtual machine image running x86-64 Arch Linux with the Coq dependencies and the typechecker pre-installed so one can validate the claims from the paper directly through the VM.

Related Organizations

University of Pennsylvania
United States

Impact byBIP!

	selected citations These citations are derived from selected sources. This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).	1
	popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network.	Average
	influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).	Average
	impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network.	Average

Found an issue? Give us feedback

1

Average

Funded by

NSF| SHF: SMALL:Dependency Tracking and Dependent Types, NSF| SHF: Small: Mechanized reasoning for functional programs