scholarly journals Program equivalence for assisted grading of functional programs

2020 ◽  
Vol 4 (OOPSLA) ◽  
pp. 1-29
Author(s):  
Joshua Clune ◽  
Vijay Ramamurthy ◽  
Ruben Martins ◽  
Umut A. Acar
Keyword(s):  
Program Equivalence

Proving optimizations correct using parameterized program equivalence

2009 ◽  
Vol 44 (6) ◽  
pp. 327-337 ◽  
Author(s):  
Sudipta Kundu ◽  
Zachary Tatlock ◽  
Sorin Lerner
Keyword(s):  
Program Equivalence

scholarly journals Gradual type theory

2021 ◽  
Vol 31 ◽  
Author(s):  
MAX S. NEW ◽  
DANIEL R. LICATA ◽  
AMAL AHMED
Keyword(s):  
Type Theory ◽  
Axiomatic Theory ◽  
Program Equivalence ◽  
Gradual Typing ◽  
Contextual Equivalence ◽  
New Perspective ◽  
Typed Languages

Abstract Gradually typed languages are designed to support both dynamically typed and statically typed programming styles while preserving the benefits of each. Sound gradually typed languages dynamically check types at runtime at the boundary between statically typed and dynamically typed modules. However, there is much disagreement in the gradual typing literature over how to enforce complex types such as tuples, lists, functions and objects. In this paper, we propose a new perspective on the design of runtime gradual type enforcement: runtime type casts exist precisely to ensure the correctness of certain type-based refactorings and optimizations. For instance, for simple types, a language designer might desire that beta-eta equality is valid. We show that this perspective is useful by demonstrating that a cast semantics can be derived from beta-eta equality. We do this by providing an axiomatic account program equivalence in a gradual cast calculus in a logic we call gradual type theory (GTT). Based on Levy’s call-by-push-value, GTT allows us to axiomatize both call-by-value and call-by-name gradual languages. We then show that we can derive the behavior of casts for simple types from the corresponding eta equality principle and the assumption that the language satisfies a property called graduality, also known as the dynamic gradual guarantee. Since we can derive the semantics from the assumption of eta equality, we also receive a useful contrapositive: any observably different cast semantics that satisfies graduality must violate the eta equality. We show the consistency and applicability of our axiomatic theory by proving that a contract-based implementation using the lazy cast semantics gives a logical relations model of our type theory, where equivalence in GTT implies contextual equivalence of the programs. Since GTT also axiomatizes the dynamic gradual guarantee, our model also establishes this central theorem of gradual typing. The model is parameterized by the implementation of the dynamic types, and so gives a family of implementations that validate type-based optimization and the gradual guarantee.

Analysing graph transformation systems through constraint handling rules

2010 ◽  
Vol 11 (1) ◽  
pp. 65-109 ◽  
Author(s):  
FRANK RAISER ◽  
THOM FRÜHWIRTH
Keyword(s):  
State Transition ◽  
Graph Transformation ◽  
Constraint Handling ◽  
Transition Systems ◽  
Rule Based ◽  
Program Equivalence ◽  
Transformation Systems ◽  
Graph Transformation Systems ◽  
State Transition Systems

AbstractGraph transformation systems (GTS) and constraint handling rules (CHR) are non-deterministic rule-based state transition systems. CHR is well known for its powerful confluence and program equivalence analyses, for which we provide the basis in this work to apply them to GTS. We give a sound and complete embedding of GTS in CHR, investigate confluence of an embedded GTS and provide a program equivalence analysis for GTS via the embedding. The results confirm the suitability of CHR-based program analyses for other formalisms embedded in CHR.

Sign in / Sign up

Export Citation Format

Share Document