Open Access. Powered by Scholars. Published by Universities.®
Physical Sciences and Mathematics Commons™
Open Access. Powered by Scholars. Published by Universities.®
- Keyword
-
- Refereed papers (6)
- Anonymity (2)
- Automated theorem proving (Coq) (1)
- Basic feasible functionals (1)
- Bounded arithmetic (1)
-
- Certified cost semantics (1)
- Circuit lower bounds (1)
- Clustering (1)
- Compositional semantics (1)
- Cryptography (1)
- Denial of service (1)
- Hidden Markov models (1)
- Higher-order complexity (1)
- Higher-type computation (1)
- Implicit computational complexity (1)
- Onion routing (1)
- Pigeonhole principle (1)
- RSA (1)
- Simulation (1)
- Tor (1)
- Type systems (1)
Articles 1 - 7 of 7
Full-Text Articles in Physical Sciences and Mathematics
Stratified Polymorphism And Primitive Recursion, Norman Danner, Daniel Leivant
Stratified Polymorphism And Primitive Recursion, Norman Danner, Daniel Leivant
Norman Danner
Natural restrictions on the syntax of the second-order (i.e., polymorphic) lambda calculus are of interest for programming language theory. One of the authors showed in Leivant (1991) that when type abstraction in that calculus is stratified into levels, the definable numeric functions are precisely the super-elementary functions (level [script E]4 in the Grzegorczyk Hierarchy). We define here a second-order lambda calculus in which type abstraction is stratified to levels up to ωω, an ordinal that permits highly uniform (and finite) type inference rules. Referring to this system, we show that the numeric functions definable in …
Adventures In Time And Space, Norman Danner, James Royer
Adventures In Time And Space, Norman Danner, James Royer
Norman Danner
This paper investigates what is essentially a call-by-value version of PCF under a complexity-theoretically motivated type system. The programming formalism, ATR, has its first-order programs characterize the polynomial-time computable functions, and its second-order programs characterize the type-2 basic feasible functionals of Mehlhorn and of Cook and Urquhart. (The ATR-types are confined to levels 0, 1, and 2.) The type system comes in two parts, one that primarily restricts the sizes of values of expressions and a second that primarily restricts the time required to evaluate expressions. The size-restricted part is motivated by Bellantoni and Cook's and Leivant's implicit characterizations of …
Circuit Principles And Weak Pigeonhole Variants, Chris Pollett, Norman Danner
Circuit Principles And Weak Pigeonhole Variants, Chris Pollett, Norman Danner
Norman Danner
This paper considers the relational versions of the surjective, partial surjective, and multifunction weak pigeonhole principles for PV, , , and formulas as well as relativizations of these formulas to higher levels of the bounded arithmetic hierarchy. We show that the partial surjective weak pigeonhole principle for formulas implies that for each k there is a string of length 22nk which is hard to block-recognize by circuits of size nk. These principles in turn imply the partial surjective principle for formulas. We show that the surjective weak pigeonhole principle for formulas in implies …
Simulation Of Circuit Creation In Tor: Preliminary Results, William Boyd, Norman Danner, Danny Krizanc
Simulation Of Circuit Creation In Tor: Preliminary Results, William Boyd, Norman Danner, Danny Krizanc
Norman Danner
We describe a methodology for simulating Tor relay up/down behavior over time and give some preliminary results.
Effectiveness And Detection Of Denial Of Service Attacks In Tor, Norman Danner, Samuel Defabbia-Kane, Danny Krizanc, Marc Liberatore
Effectiveness And Detection Of Denial Of Service Attacks In Tor, Norman Danner, Samuel Defabbia-Kane, Danny Krizanc, Marc Liberatore
Norman Danner
Tor is one of the more popular systems for anonymizing near-real-time communications on the Internet. Borisov et al. [2007] proposed a denial-of-service-based attack on Tor (and related systems) that significantly increases the probability of compromising the anonymity provided. In this article, we analyze the effectiveness of the attack using both an analytic model and simulation. We also describe two algorithms for detecting such attacks, one deterministic and proved correct, the other probabilistic and verified in simulation.
A Static Cost Analysis For A Higher-Order Language, Norman Danner, Jennifer Paykin, James Royer
A Static Cost Analysis For A Higher-Order Language, Norman Danner, Jennifer Paykin, James Royer
Norman Danner
We develop a static complexity analysis for a higher-order functional language with structural list recursion. The complexity of an expression is a pair consisting of a cost and a potential. The former is defined to be the size of the expression's evaluation derivation in a standard big-step operational semantics. The latter is a measure of the "future" cost of using the value of that expression. A translation function ||.|| maps target expressions to complexities. Our main result is the following Soundness Theorem: If t is a term in the target language, then the cost component of ||t|| is an upper …
Two Algorithms In Search Of A Type System, Norman Danner, James Royer
Two Algorithms In Search Of A Type System, Norman Danner, James Royer
Norman Danner
The authors’ ATR programming formalism is a version of call-by-value PCF under a complexity-theoretically motivated type system. ATR programs run in type-2 polynomial-time and all standard type-2 basic feasible functionals are ATR -definable ( ATR types are confined to levels 0, 1, and 2). A limitation of the original version of ATR is that the only directly expressible recursions are tail-recursions. Here we extend ATR so that a broad range of affine recursions are directly expressible. In particular, the revised ATR can fairly naturally express the classic insertion- and selection-sort algorithms, thus overcoming a sticking point of most prior implicit-complexity-based …