Export Citations
Save this search
Please login to be able to save your searches and receive alerts for new content matching your search criteria.
- research-articleJanuary 2024
Strictly Monotone Brouwer Trees for Well Founded Recursion over Multiple Arguments
CPP 2024: Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and ProofsPages 205–217https://doi.org/10.1145/3636501.3636948Ordinals can be used to prove the termination of dependently typed programs. Brouwer trees are a particular ordinal notation that make it very easy to assign sizes to higher order data structures. They extend unary natural numbers with a limit ...
- research-articleAugust 2022
Propositional equality for gradual dependently typed programming
Proceedings of the ACM on Programming Languages (PACMPL), Volume 6, Issue ICFPArticle No.: 96, Pages 165–193https://doi.org/10.1145/3547627Gradual dependent types can help with the incremental adoption of dependently typed code by providing a principled semantics for imprecise types and proofs, where some parts have been omitted. Current theories of gradual dependent types, though, lack a ...
- research-articleSeptember 2019
Insertion operations on deterministic reversal-bounded counter machines
Journal of Computer and System Sciences (JCSS), Volume 104, Issue CPages 244–257https://doi.org/10.1016/j.jcss.2018.02.003AbstractSeveral insertion operations are studied applied to languages accepted by one-way and two-way deterministic reversal-bounded multicounter machines. These operations are defined by the ideals obtained from relations such as the prefix, ...
Highlights- Insertions on deterministic reversal-bounded multicounter machines (DCM) are studied.
Approximate normalization for gradual dependent types
Proceedings of the ACM on Programming Languages (PACMPL), Volume 3, Issue ICFPArticle No.: 88, Pages 1–30https://doi.org/10.1145/3341692Dependent types help programmers write highly reliable code. However, this reliability comes at a cost: it can be challenging to write new prototypes in (or migrate old code to) dependently-typed programming languages. Gradual typing makes static type ...
- ArticleJune 2019
Set Constraints, Pattern Match Analysis, and SMT
AbstractSet constraints provide a highly general way to formulate program analyses. However, solving arbitrary boolean combinations of set constraints is -hard. Moreover, while theoretical algorithms to solve arbitrary set constraints exist, they are ...
- research-articleJune 2016
The ASPECTA toolkit: affordable full coverage displays
PerDis '16: Proceedings of the 5th ACM International Symposium on Pervasive DisplaysPages 87–105https://doi.org/10.1145/2914920.2915006Full Coverage Displays (FCDs) cover the interior surface of an entire room with pixels. FCDs make possible many new kinds of immersive display experiences - but current technology for building FCDs is expensive and complex, and software support for ...
- posterOctober 2013
The poor man's proof assistant: using prolog to develop formal language theoretic proofs
SPLASH '13: Proceedings of the 2013 companion publication for conference on Systems, programming, & applications: software for humanityPages 75–76https://doi.org/10.1145/2508075.2508088While proving a theorem from a set of axioms is undecidable in first order logic, recent development has produced several tools which serve as automated theorem provers. However, often these systems are too complex for a given problem. Their usefulness ...
- short-paperOctober 2013
The poor man's proof assistant: using prolog to develop formal language theoretic proofs
SPLASH '13: Proceedings of the 2013 companion publication for conference on Systems, programming, & applications: software for humanityPages 101–102https://doi.org/10.1145/2508075.2527300While proving a theorem from a set of axioms is undecidable in first order logic, recent development has produced several tools which serve as automated theorem provers. However, often these systems are too complex for a given problem. Their usefulness ...