Zobrazeno 1 - 10
of 10
pro vyhledávání: '"Chris Casinghino"'
Autor:
Vilhelm Sjöberg, Chris Casinghino, Ki Yung Ahn, Nathan Collins, Harley D. Eades III, Peng Fu, Garrin Kimmell, Tim Sheard, Aaron Stump, Stephanie Weirich
Publikováno v:
Electronic Proceedings in Theoretical Computer Science, Vol 76, Iss Proc. MSFP 2012, Pp 112-162 (2012)
We present a full-spectrum dependently typed core language which includes both nontermination and computational irrelevance (a.k.a. erasure), a combination which has not been studied before. The two features interact: to protect type safety we must b
Externí odkaz:
https://doaj.org/article/377d50b72b4a4b8fa419a7776956326a
Publikováno v:
Electronic Proceedings in Theoretical Computer Science, Vol 76, Iss Proc. MSFP 2012, Pp 25-39 (2012)
The Trellys project has produced several designs for practical dependently typed languages. These languages are broken into two fragments—a _logical_ fragment where every term normalizes and which is consistent when interpreted as a logic, and a _p
Externí odkaz:
https://doaj.org/article/4d24bda3067b433bad3c0fa99e8d0e9f
Publikováno v:
PLDI
Parsers are security-critical components of many software systems, and verified parsing therefore has a key role to play in secure software design. However, existing verified parsers for context-free grammars are limited in their expressiveness, term
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::f81d51c5529973b34f6cf2a0e1eeab7e
https://doi.org/10.1145/3453483.3454053
https://doi.org/10.1145/3453483.3454053
Publikováno v:
Lecture Notes in Computer Science ISBN: 9783030206512
NFM
NFM
Binary analysis frameworks are critical tools for analyzing software and assessing its security. How easy is it for a non-expert to use these tools? This paper compares two popular open-source binary analysis libraries: BAP and angr, which were used
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::09ce1e418953f82ff61bd9c687190a3e
https://doi.org/10.1007/978-3-030-20652-9_8
https://doi.org/10.1007/978-3-030-20652-9_8
Autor:
Chris Casinghino
Publikováno v:
ACM SIGAda Ada Letters. 39:71-71
No paper or presentation is available, but information on the "inherently secure processor" developed by Draper Laboratory can be found here: https://www.draper.com/explore-solutions/inherently-secure-processor
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::4b9b7e88a20e006a75cfb53b5796e6e1
https://doi.org/10.1145/3379106.3379115
https://doi.org/10.1145/3379106.3379115
Autor:
Brandon T. Shapiro, Chris Casinghino
Publikováno v:
Lecture Notes in Computer Science ISBN: 9783319572871
NFM
NFM
We present specgen, a tool for translating statecharts to the Communicating Sequential Processes language (CSP), where they may be explored and verified using FDR, the CSP model checker. We build on earlier algorithms for translating statecharts to C
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::b7ee9c1a99d6665cd92c5fad6ea97fe1
https://doi.org/10.1007/978-3-319-57288-8_19
https://doi.org/10.1007/978-3-319-57288-8_19
Autor:
Chris Casinghino, Stephanie Weirich
Publikováno v:
Lecture Notes in Computer Science ISBN: 9783642322013
SSGIP
SSGIP
Some programs are doubly generic. For example, map is datatype-generic in that many different data structures support a mapping operation. A generic programming language like Generic Haskell can use a single definition to generate map for each type.
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::a8dc35efbd9762fa4b5c475e0db861eb
https://doi.org/10.1007/978-3-642-32202-0_5
https://doi.org/10.1007/978-3-642-32202-0_5
Autor:
Chris Casinghino, Stephanie Weirich
Publikováno v:
PLPV
Some programs are doubly-generic. For example, map is datatype-generic in that many different data structures support a mapping operation. A generic programming language like Generic Haskell can use a single definition to generate map for each type.
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::a000c303636a220607a4ad22d780bdc2
https://doi.org/10.1145/1707790.1707799
https://doi.org/10.1145/1707790.1707799
Autor:
Stephanie Weirich, Chris Casinghino, Vilhelm Sjöberg, Peng Fu, Aaron Stump, Garrin Kimmell, Ki Yung Ahn, Tim Sheard, Nathan Collins, Harley Eades
Publikováno v:
PLPV
Dependently typed programming languages provide a mechanism for integrating verification and programming by encoding invariants as types. Traditionally, dependently typed languages have been based on constructive type theories, where the connection b
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::85c1abc710c3cb742aa938de0962df67
https://doi.org/10.2201/niipi.2013.10.3
https://doi.org/10.2201/niipi.2013.10.3
Publikováno v:
Scopus-Elsevier
POPL
POPL
Most dependently-typed programming languages either require that all expressions terminate (e.g. Coq, Agda, and Epigram), or allow infinite loops but are inconsistent when viewed as logics (e.g. Haskell, ATS, Ωmega. Here, we combine these two approa
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::a6d60dc0efdca058303d40f2e5385460
http://www.scopus.com/inward/record.url?eid=2-s2.0-84894060192&partnerID=MN8TOARS
http://www.scopus.com/inward/record.url?eid=2-s2.0-84894060192&partnerID=MN8TOARS