scholarly journals The use of types in designing unification algorithms: two case studies

10.29007/lbk5 ◽  
2018 ◽  
Author(s):  
Serdar Erbatur ◽  
Santiago Escobar ◽  
Paliath Narendran
Keyword(s):  
Case Studies ◽  
Type System ◽  
Equational Theory ◽  
Type Systems ◽  
Strict Sense ◽  
Signature Schemes ◽  
Rule Based ◽  
Unification Algorithms

We discuss the use of type systems in a non-strict sensewhen designing unification algorithms. We first give anew (rule-based) algorithm for an equational theory which representsa property of El-Gamal signature schemes and show howa type system can be used to prove termination of the algorithm.Lastly, we reproduce termination result for theory of partialexponentiation given earlier.

scholarly journals Dependently-typed data plane programming

2022 ◽  
Vol 6 (POPL) ◽  
pp. 1-28
Author(s):  
Matthias Eichholz ◽  
Eric Hayden Campbell ◽  
Matthias Krebs ◽  
Nate Foster ◽  
Mira Mezini
Keyword(s):  
Programming Languages ◽  
Case Studies ◽  
Type System ◽  
Type Systems ◽  
Network Data ◽  
Simple Type ◽  
Data Plane ◽  
Verification Tools

Programming languages like P4 enable specifying the behavior of network data planes in software. However, with increasingly powerful and complex applications running in the network, the risk of faults also increases. Hence, there is growing recognition of the need for methods and tools to statically verify the correctness of P4 code, especially as the language lacks basic safety guarantees. Type systems are a lightweight and compositional way to establish program properties, but there is a significant gap between the kinds of properties that can be proved using simple type systems (e.g., SafeP4) and those that can be obtained using full-blown verification tools (e.g., p4v). In this paper, we close this gap by developing Π4, a dependently-typed version of P4 based on decidable refinements. We motivate the design of Π4, prove the soundness of its type system, develop an SMT-based implementation, and present case studies that illustrate its applicability to a variety of data plane programs.

A system of constructor classes: overloading and implicit higher-order polymorphism

1995 ◽  
Vol 5 (1) ◽  
pp. 1-35 ◽  
Author(s):  
Mark P. Jones
Keyword(s):  
Type System ◽  
Type Systems ◽  
Natural Generalization ◽  
Higher Order ◽  
Functional Language ◽  
Effective Algorithm ◽  
Prototype Implementation ◽  
Type Classes

AbstractThis paper describes a flexible type system that combines overloading and higher-order polymorphism in an implicitly typed language using a system of constructor classes—a natural generalization of type classes in Haskell. We present a range of examples to demonstrate the usefulness of such a system. In particular, we show how constructor classes can be used to support the use of monads in a functional language. The underlying type system permits higher-order polymorphism but retains many of the attractive features that have made Hindley/Milner type systems so popular. In particular, there is an effective algorithm that can be used to calculate principal types without the need for explicit type or kind annotations. A prototype implementation has been developed providing, amongst other things, the first concrete implementation of monad comprehensions known to us at the time of writing.

scholarly journals Dynamic Question Ordering in Online Surveys

2017 ◽  
Vol 33 (3) ◽  
pp. 625-657 ◽  
Author(s):  
Kirstin Early ◽  
Jennifer Mankoff ◽  
Stephen E. Fienberg
Keyword(s):  
Case Studies ◽  
Survey Methodology ◽  
Response Rate ◽  
General Survey ◽  
Online Surveys ◽  
Rule Based ◽  
Past Work ◽  
National Surveys ◽  
Question Order ◽  
Rule Based Approach

Abstract Online surveys have the potential to support adaptive questions, where later questions depend on earlier responses. Past work has taken a rule-based approach, uniformly across all respondents. We envision a richer interpretation of adaptive questions, which we call Dynamic Question Ordering (DQO), where question order is personalized. Such an approach could increase engagement, and therefore response rate, as well as imputation quality. We present a DQO framework to improve survey completion and imputation. In the general survey-taking setting, we want to maximize survey completion, and so we focus on ordering questions to engage the respondent and collect hopefully all information, or at least the information that most characterizes the respondent, for accurate imputations. In another scenario, our goal is to provide a personalized prediction. Since it is possible to give reasonable predictions with only a subset of questions, we are not concerned with motivating users to answer all questions. Instead, we want to order questions to get information that reduces prediction uncertainty, while not being too burdensome. We illustrate this framework with two case studies, for the prediction and survey-taking settings. We also discuss DQO for national surveys and consider connections between our statistics-based question-ordering approach and cognitive survey methodology.

scholarly journals Automating Proof Steps of Progress Proofs: Comparing Vampire and Dafny

10.29007/5zjp ◽  
2018 ◽  
Author(s):  
Sylvia Grewe ◽  
Sebastian Erdweg ◽  
Mira Mezini
Keyword(s):  
Formal Methods ◽  
Programming Language ◽  
Type System ◽  
Type Systems ◽  
Domain Specific Languages ◽  
Smt Solver ◽  
Domain Specific ◽  
Efficient Type

\noindent Developing provably sound type systems is a non-trivial task which, as of today, typically requires expert skills in formal methods and a considerable amount of time. Our Veritas~\cite{GreweErdwegWittmannMezini15} project aims at providing support for the development of soundness proofs of type systems and efficient type checker implementations from specifications of type systems. To this end, we investigate how to best automate typical steps within type soundness proofs.\noindent In this paper, we focus on progress proofs for type systems of domain-specific languages. As a running example for such a type system, we model a subset SQL and augment it with a type system. We compare two different approaches for automating proof steps of the progress proofs for this type system against each other: firstly, our own tool Veritas, which translates proof goals and specifications automatically to TPTP~\cite{Sutcliffe98} and calls Vampire~\cite{KovacsV13} on them, and secondly, the programming language Dafny~\cite{Leino2010}, which translates proof goals and specifications to the intermediate verification language Boogie 2~\cite{Leino2008} and calls the SMT solver Z3~\cite{DeMoura2008} on them. We find that Vampire and Dafny are equally well-suited for automatically proving simple steps within progress proofs.

How to evaluate the performance of gradual type systems

2019 ◽  
Vol 29 ◽  
Author(s):  
BEN GREENMAN ◽  
ASUMU TAKIKAWA ◽  
MAX S. NEW ◽  
DANIEL FELTEY ◽  
ROBERT BRUCE FINDLER ◽  
...  
Keyword(s):  
Type System ◽  
Type Systems ◽  
Relative Performance ◽  
Systematic Evaluation ◽  
Gradual Typing ◽  
The Absolute

Abstract A sound gradual type system ensures that untyped components of a program can never break the guarantees of statically typed components. This assurance relies on runtime checks, which in turn impose performance overhead in proportion to the frequency and nature of interaction between typed and untyped components. The literature on gradual typing lacks rigorous descriptions of methods for measuring the performance of gradual type systems. This gap has consequences for the implementors of gradual type systems and developers who use such systems. Without systematic evaluation of mixed-typed programs, implementors cannot precisely determine how improvements to a gradual type system affect performance. Developers cannot predict whether adding types to part of a program will significantly degrade (or improve) its performance. This paper presents the first method for evaluating the performance of sound gradual type systems. The method quantifies both the absolute performance of a gradual type system and the relative performance of two implementations of the same gradual type system. To validate the method, the paper reports on its application to 20 programs and 3 implementations of Typed Racket.

scholarly journals Pure Type System conversion is always typable

2012 ◽  
Vol 22 (2) ◽  
pp. 153-180 ◽  
Author(s):  
VINCENT SILES ◽  
HUGO HERBELIN
Keyword(s):  
Type System ◽  
Type Systems ◽  
Positive Answer ◽  
General Question ◽  
Pure Type ◽  
Typing System ◽  
Long Time ◽  
Pure Type Systems

AbstractPure Type Systems are usually described in two different ways, one that uses an external notion of computation like beta-reduction, and one that relies on a typed judgment of equality, directly in the typing system. For a long time, the question was open to know whether both presentations described the same theory. A first step towards this equivalence has been made by Adams for a particular class ofPure Type Systems(PTS) called functional. Then, his result has been relaxed to all semi-full PTSs in previous work. In this paper, we finally give a positive answer to the general question, and prove that equivalence holds for any Pure Type System.

Introduction to the Special Issue on Dependent Type Theory Meets Practical Programming

2004 ◽  
Vol 14 (1) ◽  
pp. 1-2
Author(s):  
GILLES BARTHE ◽  
PETER DYBJEN ◽  
PETER THIEMANN
Keyword(s):  
Programming Languages ◽  
Type Theory ◽  
Type System ◽  
Type Systems ◽  
Special Issue ◽  
Dependent Type Theory ◽  
Dependent Type

Modern programming languages rely on advanced type systems that detect errors at compile-time. While the benefits of type systems have long been recognized, there are some areas where the standard systems in programming languages are not expressive enough. Language designers usually trade expressiveness for decidability of the type system. Some interesting programs will always be rejected (despite their semantical soundness) or be assigned uninformative types.

scholarly journals Implicit self-adjusting computation for purely functional programs

2014 ◽  
Vol 24 (1) ◽  
pp. 56-112 ◽  
Author(s):  
YAN CHEN ◽  
JOSHUA DUNFIELD ◽  
MATTHEW A. HAMMER ◽  
UMUT A. ACAR
Keyword(s):  
Programming Languages ◽  
Type System ◽  
Type Systems ◽  
Type Inference ◽  
Source Program ◽  
Target Program ◽  
Implicit Approach ◽  
Asymptotic Complexity ◽  
Cost Semantics ◽  
Output Behavior

AbstractComputational problems that involve dynamic data, such as physics simulations and program development environments, have been an important subject of study in programming languages. Building on this work, recent advances in self-adjusting computation have developed techniques that enable programs to respond automatically and efficiently to dynamic changes in their inputs. Self-adjusting programs have been shown to be efficient for a reasonably broad range of problems, but the approach still requires an explicit programming style, where the programmer must use specific monadic types and primitives to identify, create, and operate on data that can change over time. We describe techniques for automatically translating purely functional programs into self-adjusting programs. In this implicit approach, the programmer need only annotate the (top-level) input types of the programs to be translated. Type inference finds all other types, and a type-directed translation rewrites the source program into an explicitly self-adjusting target program. The type system is related to information-flow type systems and enjoys decidable type inference via constraint solving. We prove that the translation outputs well- typed self-adjusting programs and preserves the source program's input–output behavior, guaranteeing that translated programs respond correctly to all changes to their data. Using a cost semantics, we also prove that the translation preserves the asymptotic complexity of the source program.

Sign in / Sign up

Export Citation Format

Share Document