| |
|
|
| |
| |
|
Date Reviewed |
|
| |
1 - 10 of 29
reviews
|
|
|
 |
|
|
|
|
Cubical Agda: a dependently typed programming language with univalence and higher inductive types
Vezzosi A., Mörtberg A., Abel A. Proceedings of the ACM on Programming Languages 3(ICFP): 1-29, 2019. Type: Article
Russell proposed type theory in the first decades of the 20th century in response to the foundational crisis faced by set theory. Over the last century, there have been a number of developments in type theory, in particular the mechani...
|
Jul 23 2021 |
|
|
|
|
|
|
Implicit parameters for logic programming
Madsen M., Lhoták O. PPDP 2018 (Proceedings of the 20th International Symposium on Principles and Practice of Declarative Programming, Frankfurt am Main, Germany, Sep 3-5, 2018) 1-14, 2018. Type: Proceedings
The art of programming is all about building programs that are concise, elegant, efficient, and, most importantly, readable and understandable by others. Software engineers use a number of tools to make code readable, for example, well...
|
Mar 10 2021 |
|
|
|
|
|
|
RDF multi-query optimization algorithm for query rewriting using common subgraphs
Wang M., Fu H., Xu F. CSAE 2019 (Proceedings of the 3rd International Conference on Computer Science and Application Engineering, Sanya, China, Oct 22-24, 2019) 1-8, 2019. Type: Proceedings
Resource description framework (RDF) is a data representation standard for loosely structured data that can be used to represent large datasets that arise in applications such as social networks. The challenge of searching and analyzin...
|
Aug 17 2020 |
|
|
|
|
|
|
Variant construction from theoretical foundation to applications
Zheng J., Springer International Publishing, New York, NY, 2019. 409 pp. Type: Book
This book is a collection of chapters authored primarily by Jeffrey Zheng, who is also the editor. The preface lays out a broad roadmap for expanding vector 0-1 logical systems, highlighting the areas of variant logic, variant measurem...
|
Nov 11 2019 |
|
|
|
|
|
|
STADS: software testing as species discovery
Böhme M. ACM Transactions on Software Engineering and Methodology 27(2): 1-52, 2018. Type: Article
Software testing is an exercise in extrapolation--we attempt to infer the correctness of software by exercising it using test cases. However, as Dijkstra famously observed, testing demonstrates the presence of bugs, not their ...
|
Jan 17 2019 |
|
|
|
|
|
|
Generalizing Morley’s and other theorems with automated realization
Braude E., Abdyldayev S. Journal of Automated Reasoning 60(4): 503-526, 2018. Type: Article
Progress in the area of automated theorem proving has been traditionally demonstrated by automatically and mechanically proving conjectures and theorems in classical mathematics. Examples include the proof of the four-color theorem and...
|
Oct 10 2018 |
|
|
|
|
|
|
A compositional modelling and verification framework for stochastic hybrid systems
Wang S., Zhan N., Zhang L. Formal Aspects of Computing 29(4): 751-775, 2017. Type: Article
The need to explore new formalisms for specifying, implementing, and verifying systems is driven by the increasing complexity of systems we wish to analyze and synthesize. At the same time, there is a growing realization of the need fo...
|
Mar 29 2018 |
|
|
|
|
|
|
Semantics-based program verifiers for all languages
Stefănescu A., Park D., Yuwen S., Li Y., Roşu G. OOPSLA 2016 (Proceedings of the 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, Amsterdam, Netherlands, Nov 2-4, 2016) 74-91, 2016. Type: Proceedings
Programming is hard. Verifying correctness of a program is harder. Building an automated tool for program verification is harder still: there are very few tools that can perform verification of non-trivial programs written in real-worl...
|
Jul 20 2017 |
|
|
|
|
|
|
Foundations for using linear temporal logic in Event-B refinement
Hoang T., Schneider S., Treharne H., Williams D. Formal Aspects of Computing 28(6): 909-935, 2016. Type: Article
Event-B is a formal method for system-level modeling and analysis. In the last decade, Event-B refinement has generated a lot of interest as a formalism for developing highly reliable software. The Event-B language, along with tools su...
|
Apr 12 2017 |
|
|
|
|
|
|
Modelling timed reactive systems from natural-language requirements
Carvalho G., Cavalcanti A., Sampaio A. Formal Aspects of Computing 28(5): 725-765, 2016. Type: Article
Automated verification of software systems is an important area of current research in both academia and industry. Such methods have the potential to considerably reduce the cost of verification. Such techniques, however, depend on hav...
|
Mar 7 2017 |
|
|
|
|
|
| |
|
|
| |
|
|
